# in refutation (resolution) can we use a clause that have been resolved

In resolution if we have a set S composed of three clause C1, C2 and C3 and we want to proof that C4 is derivable from S using refutation:

suppose we've resolved C1 and C2 to C5, can we resolve C1 with C5 or C3 or C4 or C2 cause even it has been resolved?

and if we want to conceive an algorithm for that do we have to delete each resolved couple of clauses from or initial set I= {S, ¬C4} and add the resolvent instead?

and lastly, do we have to use all the clause to derive ⊥ or we stop once we find ⊥ even if we find it in the first step?

thank you for claryfing things.

suppose we've resolved C1 and C2 to C5, can we resolve C1 with C5 or C2?

No, not really. If C1 and C2 can be resolved in more than one way, then all those resolvents are tautologies. And if C1 can be resolved with C5, then it can also be resolved with C2 in a second way (assuming C1 is not a tautology, and hence cannot be resolved with itself).

can we resolve C1 with C3 or C4 cause even it has been resolved?

We can (and often must) resolve C1 with C3, even so it has already been resolved with C2. We don't need to resolve any clause with C4 itself, rather the negation of C4 must be brought into a conjunctive normal form. The clauses of that normal for have to be added to our set S.

and if we want to conceive an algorithm for that do we have to delete each resolved couple of clauses from our initial set I= {S, ¬C4} and add the resolvent instead?

No, that would be too simple. What you actually do is to select a variable that you want to eliminate from the clauses in the set S, and then:

• for every clause C containing the variable and every clause N containing the negation of the variable
• resolve C and N and add the resolvent to the set S
• remove all original clauses containing the variable or its negation from the set S

Of course, you could also eliminate a variable by considering both possible assignments separately. It is said that those two approaches are equivalent in a certain sense, yet the approach to consider the assignments separately allows for backtracking, which keeps the memory consumption low by removing the need for explicit representation of the resolvents.

and lastly, do we have to use all the clause to derive ⊥ or we stop once we find ⊥ even if we find it in the first step?

We stop once we find ⊥.

thank you for claryfing things.

The question is tagged , but none of your questions even touched unification. Your questions also indicate that the resolution rule somehow seems to feel like magic to you. But the resolution rule itself is basically just the cut rule, which is an inference rule of sequent calculus:
$\cfrac{\Gamma \vdash \Delta, A \qquad A, \Gamma' \vdash \Delta'} {\Gamma, \Gamma' \vdash \Delta, \Delta'}$

The cut rule itself is just the appropriate formulation of transitivity of implication
$\cfrac{A \vdash B \qquad B \vdash C} {A \vdash C}$
in the context of sequent calculus (where you can have both a left ($\Gamma$) and a right ($\Delta$) context). A sequent $A_1,\dots,A_r \vdash B_1,\dots,B_s$ can be read as $(A_1\land\dots\land A_r) \to (B_1\lor\dots\lor B_s)$, which is equivalent to the clause $\lnot A_1\lor\dots\lor \lnot A_r \lor B_1\lor\dots\lor B_s$.

Whether this is helpful or not is of course a matter of taste. By getting rid of negation, one can write down deductions more symmetrically (and the sequent calculus has established conventions avoiding all those dots when writing things down). You could verify the assertion that "If C1 and C2 can be resolved in more than one way, then all those resolvents are tautologies." for example by checking that the deductions
$\cfrac{\Gamma \vdash B, \Delta, A \qquad A, \Gamma', B \vdash \Delta'} {\Gamma, \Gamma', B \vdash B, \Delta, \Delta'}$ and $\cfrac{\Gamma, B \vdash \Delta, A \qquad A, \Gamma' \vdash B, \Delta'} {\Gamma, B, \Gamma' \vdash \Delta, B, \Delta'}$
cover all relevant cases.

• thank you very much for your responses and for additional explanations. – younes zeboudj Jan 4 '17 at 17:47