Logic for Computer Scientists/Propositional Logic/Resolution

Resolution edit

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

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

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

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

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

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

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

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

Problem 23 (Propositional) edit

Compute   for all   and   for the following set of clauses:

  1.  
  2.  
  3.  
  4.  

Which formula is satisfiable or which is unsatisfiable?
 

Problem 24 (Propositional) edit

Indicate all resolvent of the clauses in S, where  
 

Problem 25 (Propositional) edit

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

Problem 26 (Propositional) edit

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

  iff   is unsatisfiable.


 

Problem 27 (Propositional) edit

Compute   with   and

 
 

Problem 28 (Propositional) edit

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

Problem 29 (Propositional) edit

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

Problem 30 (Propositional) edit

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