Let's say we have the following rule:

p -: X ≠ Y, X = Y

Stating that $\forall x.y. x \neq y \land x = y \implies p$. Now let us suppose that we are searching for a proof of $p$. Such a proof does not exist, of course, but we will search for it.

Our starting goal is p. We replace it with the subgoals X ≠ Y and X = Y. To resolve X ≠ Y, we use negation as failure. We must show that exists an $x$ and $y$ such that $x = y$ is unprovable. So we know have a goal of X = Y. Since $x$ and $y$ are not the same variable (remember, $x$ and $y$ were bound by the quantifier of the top level rule), there is no way to resolve $x = y$. So we fail to show $x = y$, and the subgoal X ≠ Y is resolved. We now resolve the subgoal X = Y. This is done by unification, which means we set Y := X. Since all subgoals have been resolved, the original goal p has succeeded, with the solution X := X and Y := X.

However, this is obviously incorrect since $p$ should not be provable. $x \neq y \land x = y$ is always false, so we can not use the rule to deduce it.

The problem seems to be that negation as failure is not actually negation. Being unable to show that $x \neq y$ does not mean it is false. Resolving something like I did above "loses" consequences of negated statements.

What is the correct way to resolve rules like the above?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.