Logic for Computer Scientists/Propositional Logic/Resolution

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Resolution[edit | edit source]

In this subsection we will develop a calculus for propositional logic. Until now we have a language, i.e. a set of formulae and we have investigated into semantics and some properties of formulae or sets of clauses. Now we will introduce an inference rule, namely the resolution rule, which allows to derive new clauses from given ones.

Definition 10[edit | edit source]

A clause is a resolvent of clauses and , if there is a literal and and

where

Note that there is a special case, if we construct the resolvent out of two literals, i.e. and can be resolved upon and yield the empty set. This empty resolvent is depicted by the special symbol .
denotes an unsatisfiable formula. We define a clause set, which contains this empty clause to be unsatisfiable,

In the following we investigate in properties of the resolution rule and the entire calculus. The following Lemma is stating the correctness of one single application of the resolution rule.

Theorem 7[edit | edit source]

If is a set of clauses and a resolvent of , then

Proof: Let be an assignment for ; hence it is an assignment for as well. Assume : hence for all clauses from , we have that . The resolvent of and looks like:

where and . Now there are two cases:

  • : From and , we conclude and hence .
  • : From we conclude and hence . The opposite direction of the lemma is obvious.

Definition 11[edit | edit source]

Let be s set of clauses and

then




If we understand the process of iterating the Res-operator as a procedure for deriving new clauses from a given set, and in particular to derive possibly the empty clause, we have to ask, under which circumstances we get the empty clause, and vice versa, what does it mean if we get it. These properties are investigates in the following two Theorems.

Theorem 8 (Correctness)[edit | edit source]

Let be a set of clauses. If then is unsatisfiable.

Proof: From we conclude, that is obtained by resolution from two clauses and . Hence there is a such that and and therefore is unsatisfiable. From Theorem (resolution-lemma) we conclude that and hence is unsatisfiable.

Theorem 9 (Completeness)[edit | edit source]

Let be a finite set of clauses. If is unsatisfiable then .

Proof: Induction over the number of atomic formulae in . With we have and hence .

Assume fixed and for every unsatisfiable set of clauses with atomic formulae it holds that .

Assume a set of clauses with atomic formulae . In the following we construct two clause sets and :

  • is received from by deleting every occurrence of in a clause and by deleting every clause which contains an occurrence of . This transformation obviously corresponds to interpreting the atom with ,
  • results from a similar transformation, where occurrences of and clauses containing are deleted, hence is interpreted with .

Let us show, that both and are unsatisfiable: Assume an assignment for the atomic formale which is a model for . Hence the assignment is a model for , which leads to a contradiction. A similar construction shows that is unsatisfiable. Hence then we can use the induction assumption to conclude that and . Hence there is a sequence of clauses

such that it holds or is a resolvent of two clauses and with .There is an analog sequence for :

Now we are going to reintroduce the previously deleted literals and in the two sequences:

  • Clause which has been the result of deleting from the original clause in are again modified to . This results in a sequence

where is either or .

  • Analogous we introduce in the second sequence, such that is either or

In any of the above cases we get latest after one resolution step with and .


Based on the theorems for correctness and completeness, we give a procedure for deciding the satisfiability of propositional formulae.

Deciding Satisfiability of Propositional Formulae

Given a propositional formula .

  • Transform into an equivalent CNF .
  • Compute for
    • If then Stop: unsatisfiable .
    • if then Stop: satisfiable .

Theorem 10[edit | edit source]

If is a finite set of clauses, then there exists a such that


Until now, we have been dealing with sets of clauses. In the following it will turn out, that it is helpful to talk about sequences of applications of the resolution rule.

Definition 12[edit | edit source]

A deduction of a clause from a set of clauses is a sequence , such that

  • and


A deduction of the empty clause from is called a refutation of .


Example We want to show, that the formula is a logical consequence of . For this negate and prove the unsatisfiability of

For this you can use the interaction in this book in various forms:

  • Use the interaction Truth Tables for proving the unsatisfiability, or
  • use the interaction CNF Transformation for transforming the formula into CNF, and then
  • use the following interaction Resolution.


Problems[edit | edit source]

Problem 23 (Propositional)[edit | edit source]

Compute for all and for the following set of clauses:

Which formula is satisfiable or which is unsatisfiable?

Problem 24 (Propositional)[edit | edit source]

Indicate all resolvent of the clauses in S, where

Problem 25 (Propositional)[edit | edit source]

Prove: A resolvent of two clauses and is a logical consequence from and . Note: Use the definition of "consequence".

Problem 26 (Propositional)[edit | edit source]

Let be a set of formulae and a formula. Prove:

iff is unsatisfiable.


Problem 27 (Propositional)[edit | edit source]

Compute with and


Problem 28 (Propositional)[edit | edit source]

Show that the following set of formulae is unsatisfiable, by giving a refutation.

Problem 29 (Propositional)[edit | edit source]

Show by using the resolution rule, that is an inference from the set of clauses .

Problem 30 (Propositional)[edit | edit source]

Show by using the resolution rule, that is a tautology.