# Distinct variables for different clauses

In resolution theorem proving, it is normally assumed variables in different clauses are distinct. This is not something that happens automatically; it requires significant extra code and computation to implement. Given that, I'm looking for a test case for it.

The problem is, in all the test cases I've tried so far, it makes no difference. Presumably it matters only in unusual edge cases. As Wikipedia puts it, "variables in different clauses are distinct... Now, unifying Q(X) in the first clause with Q(Y) in the second clause means that X and Y become the same variable anyway."

Are there any known test cases that will actually give the wrong answer if different clauses use the same variables?

-

Edit: I found a better example. Consider these clauses: \begin{align} & \lnot P(x) \lor P(f(x)) \\ & P(x) \\ & \lnot P(f(f(x)))\\ \end{align} Obviously, this set of clauses is contradictory. But without renaming variables, the only possible resolvent is $P(f(x))$ and no more resolvents are possible - all lead to substituting $f(x)$ for $x$, which is impossible.

Edit: Consider the meaning of clauses. Each clause is implicitly universally quantified. So the meaning of its variables isn't fixed to anything. Now let's say you have two clauses both containing $x$. If you perform resolution without renaming $x$ in one of them, then you add a meaning to $x$ which it doesn't have: you say that $x$ means the same thing in both clauses, which is not true. If you don't have distinct variables in your clauses, resolution will give you too weak conclusions.

(The original answer.) For example, let's have 4 clauses:

1. $A\lor B(x)$
2. $\lnot A\lor C(x)$
3. $\lnot B(c)$
4. $\lnot C(d)$

where $x, y$ are variables and $c, d$ constants. If we perform resolution on the first two without renaming $x$, we'll get $B(x)\lor C(x)$. We can proceed with $\lnot B(c)$ to get $C(c)$ but now we cannot resolve it with $\lnot C(d)$.

On the other hand, if we rename $x$ to $y$ in the second one to have disjoint set of variables, we'll get $B(x)\lor C(y)$ from the first resolution step and we can derive an empty clause using $\lnot B(c)$ and $\lnot B(d)$.

-
When I try this in my prover with distinct variables disabled, it resolves $B(x)$ with $\lnot B(c)$ to give $A$, similarly obtains $\lnot A$ and thence the empty clause, so the end result is the same. Am I missing something? –  rwallace Sep 6 '12 at 15:31
@rwallace Not having distinct variables doesn't mean you cannot derive the empty clause, just that the methods isn't complete. If you always rename variables then it doesn't matter in which order you pick clauses, you'll always derive the empty clause if the original set is unsatisfiable - the method is complete. But, if you don't rename variables then (as the example shows) the order suddenly matters - some sequences of derivations won't find the empty clause. And, a prover cannot "tell" in advance which sequence of derivations is the proper one. –  Petr Pudlák Sep 6 '12 at 16:05
But is it not the case that a complete method must eventually try every possible derivation (unless it finds the empty clause first)? To be sure there is no guarantee it will try the derivations I mentioned before the ones you mentioned, but when the ones you mentioned fail because of lack of distinct variables, the ones I mentioned are still open and a complete method must go back and try those sooner or later? –  rwallace Sep 6 '12 at 16:09
Your addendum regarding the meaning of clauses in the abstract makes sense, but it seems to me if that is so then it ought to be possible to find a test case, something I can feed into a prover and cause it to give the wrong answer if the distinct variables feature is disabled. I just haven't been able to find such a test case so far. –  rwallace Sep 6 '12 at 16:23
@rwallace Why would you want to do that? Resolution is a complete method and you know that under any circumstances it's only necessary to perform resolution on each pair of clauses only once. You suggest to eventually try all possible sequences how to proceed with backtracking. This will result in a really huge increase of the algorithm's complexity, not even remotely comparable with simply renaming variables at each step. –  Petr Pudlák Sep 6 '12 at 16:24