1

I know the theorem of "Completeness for Resolution principle", but i have a question :

if the resolution principle is complete, this means that via only the binary resolution we are able to find EVERY logical consequence of the initial set of clauses .

However the resolution principle uses the modus ponens and we know that there exist other inference rules beyond it, like generalization. Why the modus ponens is able to generate by itself every possible logical consequence?

Qwerto
  • 969
  • 6
  • 20
  • Please note that the resolution method is not able to derive every logical consequence. E.g. Starting with $P$, you cannot get $P \lor Q$. Completeness of resolution means that if the original clause set is inconsistent, then the empty clause can be derived. – Bram28 Mar 04 '18 at 13:26

1 Answers1

3

When applied to FOL, the Resolution technique presupposes:

  • first, that the formulas must be "skolemized", with all quantification becomes implicit: universal quantifiers are simply omitted as understood, while existentially-quantified variables are replaced by Skolem functions

  • second: clauses must be converted to conjunctive normal form.

After the above transformations, the problem is reduced to as "propostional problems" (the caluses contain only atoms), where modus ponens suffices.

The inference rule used in the various algorithmic implementations of Resoution is refutation-complete, meaning that a set of clauses is unsatisfiable if and only if there exists a derivation of the empty clause using resolution alone.

See: Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), Chapter 10: First-Order Logic: Resolution, for a complete treatment, and see page 200:

Completeness of resolution: If a set of clauses is unsatisfiable, the empty clause can be derived by the resolution procedure.

Also very useful: Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press (1973).

Mauro ALLEGRANZA
  • 94,169