4
$\begingroup$

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?

$\endgroup$

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.