I have the following sentence.

$(A ∨ (B ∧ C) ∨ (¬A ∧ ¬B) ∨ (¬A ∧ B ∧ ¬C))$

I am having difficulty understanding how to apply the resolution method.

What (I think) I know so far:

In terms of resolution as it applies to my problem, it seems I am considering the resolution technique (of propositional logic).

Given the resolution technique in the following form:

$$\underline{\{Q ∧ O\} \ \{¬O\}}$$ $$Q$$

To put it in my own words, the resolution technique reduces a sentence to a set of clauses of literals and considers which what the value of each literal would have to be such that the conjunction of each clause would be true. So in my cause I need to:

  1. Rearrange my sentence to a set of clauses.
  2. Determine the value for each literal, using the technique above.
  3. Use the information from step 2 to determine weather the sentence is a tautology (I don't know how to do this).

Am I on the right track? Any tips?


See Resolution (logic) :

the resolution technique uses proof by contradiction and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in Conjunctive Normal Form.

1st step :

the negation of the sentence to be proved (the conjecture) is to be considered.

In your case, we have :

$$\lnot [A ∨ (B∧C) ∨ (¬A∧¬B) ∨ (¬A∧B∧¬C)] \equiv [¬A ∧ (¬B ∨ ¬C) ∧ (A ∨ B) ∧ (A ∨ ¬B ∨ C)].$$

As said above, the proof procedure works by contradicition : assume the formula $\lnot \varphi$ (where $\varphi$ is the conjecture) and apply iteratively the rule.

If the procedure gives us as result that the formula $\lnot \varphi$ is unsatisfiable, we can conclude that the original conjecture ($\varphi$) is a tautology.

2nd step :

the sentence is transformed into a Conjunctive Normal Form with the conjuncts viewed as elements in a set, $S$, of clauses, where a clause is a disjunction of literals.

Thus, the formula above will correspond to the set of clauses :

$S = \{ ¬A, (¬B ∨ ¬C), (A ∨ B), (A ∨ ¬B ∨ C) \}$.

3rd step :

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 $S$, it is added to $S$, and is considered for further resolution inferences.

If after applying a resolution rule the empty clause, $\square$ (or : $\bot$), is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture is a tautology.

We have to apply the rule to the set $S$ above :

1) $¬A$

2) $¬B ∨ ¬C$

3) $A ∨ B$

4) $A ∨ ¬B ∨ C$

5) $B$ --- from 1) and 3)

6) $¬B ∨ C$ --- from 1) and 4)

7) $¬C$ --- from 5) and 2)

8) $C$ --- from 5) and 6)

$\square$ --- the empty clause : from 7) and 8).

The rule has the property that preserves satisfiability, i.e. the new set of clauses is satisfiable iff the original one is.

Thus, if after iterated applications of the rule the empty clause is produced, being it unsatisfiable (the empty clause in another way of representing a contradiction) this is enough to conclude that also the original set of clauses is unsatisfiable.

  • $\begingroup$ >the negation of the sentence to be proved (the conjecture) is to be considered. @Mauro would you mind adding a little bit of clarification to this point? $\endgroup$
    – Oscar
    Jun 26 '18 at 12:47
  • $\begingroup$ my reference text is "Language, Proof and Logic" (J. Barwise, J. Etchemendy). I know see that "To show that a sentence is logically true, we need only show that its negation is not satisfiable" p 492, task 17.35, so I missed this piece of information. $\endgroup$
    – Oscar
    Jun 26 '18 at 13:03
  • $\begingroup$ @Oscar - perfect: that property is the key-point of resolution proof procedure :-) $\endgroup$ Jun 26 '18 at 13:08
  • $\begingroup$ yes, that property was certainly not a good piece of information to have missed. But thanks to your help I am now aware of it :) Thanks for the very thorough answer, I will review it shortly $\endgroup$
    – Oscar
    Jun 26 '18 at 13:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.