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?
