TITLE: Trouble with step 2 resolution calculus
QUESTION [0 upvotes]: I need to prove T ⊨ A v B with the resolution calculus from a set T.
Step 1
Transform T into a set of clauses (CNF).

Clause 1 = A v ¬C
Clause 2 =  C v A v B

Step 2
Try to find a resolution proof for ⊥, that is T ∪ {¬A ∧ ¬B}. Resolve Clause 1 (A v ¬C) and Clause 2 (C v A v B)
I understand I must find some kind of contradiction and there out conclude T ⊨ A v B. 
I am really lost, not sure how to begin, all I can determine is that if C is true in one clause that it is false in the other (and vica versa).
How do I continue?

REPLY [0 votes]: To prove that $T \vDash \varphi$ we have to apply Resolution to the set $T \cup \{ ¬ \varphi \}$.
Thus, as you say, we have to consider the set of clauses:

$\{ A \lor \lnot C, A \lor B \lor C, \lnot A, \lnot B \}$

built up with Clause 1, Clause 2 and the two clauses produced from the negation of the conclusion: $\lnot (A \lor B) \equiv (\lnot A \land \lnot B)$.
The aim of the procedure is to derive the empty clause: $\bot$ or $\square$.
If so, we have proved that the set is unsatisfiable (or contradictory), and hence we can conclude that the original sought conclusion (the formual we have negated) follows from $T$.

The steps of the procedure are :
1) All premises and the negation of the sentence to be proved (the conclusion) are conjunctively connected.
2) The resulting sentence is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set of clauses.
3) The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set, it is added to it, and is considered for further resolution inferences.
4) If after applying a resolution rule the empty clause is derived, the original set of clauses is unsatisfiable.
5) If, on the other hand, the empty clause cannot be derived, and the resolution rule cannot be applied to derive any more new clauses, the formula to be proved is not a consequence of the original premises.
In your example, we have to start with :
1) $A \lor \lnot C$
2) $A \lor B \lor C$
3) $\lnot A$
4) $\lnot B$ 
and apply the resolution rule to 1) and 2) producing:
5) $A \lor B$.
Now we can resolve 3) and 5) deriving:
6) $B$.
Finally, we resolve 4) and 6) deriving $\bot$.
{"set_name": "stack_exchange", "score": 0, "question_id": 1652268}