Logic for Computer Scientists/Predicate Logic/Resolution

Resolution edit

In the propositional case we defined the resolution inference rule by "cutting away" a pair of complementary literals in two clauses which are resolved upon. In the first order case however this is not always sufficient:

 

In these two clauses there are no complementary literals, however, after substituting the term   for the variable   in   and   for   in   we arrive at:

 

Now we can apply the inference rule from propositional logic and arrive at the resolvent  .

Another possibility is to substitute   for   in   to get

 

and then we can have the resolvent   from   and  , which is in a certain sense more general then the resolvent derived previously.

Definition 18 edit

A substitution   is a function, which maps variables to terms and which is the identical mapping almost everywhere. Hence it can be represented as

 

If   are groundterms, we call   a ground substitution. The empty substitution is notated by   .

Definition 19 edit

Let   be a substitution and   an expression (i.e. a literal or a term), then   is the expression, obtained from   by replacing simultaneously each occurrence of   in   by the term  .

Example:
With   and  , we get  

Definition 20 edit

Let   and   be substitutions. Then the composition of substitutions, denoted by  , is the substitution, which is obtained from   by deleting any element   for which   and any element   such that   .
Example:

Definition 21 edit

Let   be a set of expressions and   a substitution,   is unifier for   iff

 

.

A unifier   is called most general unifier iff for every unifier   there is a substitution   such that  .

In the following we discuss an algorithm for computing most general unifiers. For this we assume a set of terms   to be unified. First we transform this into a set of equations by introducing a new variable not yet occurring in this set, say   and by defining the set of equations

 

We will now transform this set such that its unifiers stay invariant, where a   is a unifier of a set of   if   holds.

Unification


Given a set of expression. Transform it into a set of equations   as defined above. Apply the following transformation rules as long as possible:

  1.   Orient

    where   is a variable and   a non-variable term

  2.   Delete

  3.   Decompose (Termreduction)

  4.   Eliminate (Elimination of variable I)

    if   not in  , but in  

  5.  Coalesce (Elimination of variable II)

    if   in  

  6.   Conflict

    if   or  

  7.   Occur Check

    if   in  

Theorem 7 edit

Let   be a set of expressions. The above unification algorithm terminates. If it returns  , there is no unifier for  , otherwise   is transformed into a set of equation  , which represents the most general unifier for  .

Definition 22 edit

Let two or more literals of a clause   have a unifier  , then   is called a factor of  .

Example:
With   and   we get the factor  

Definition 23 edit

Let   and   be two clauses with no variables in common, such that   and   and   and   have a most general unifier  . A binary resolvent of   and   is

 


Example: Given   and  . After renaming   into   we get the resolvent   by using the most general unifier  .


We often depict resolvent graphically, e.g.

 

Definition 24 edit

A resolvent of two clauses   and   is one of the following binary resolvents:

  • a binary resolvent of   and  
  • a binary resolvent of   and a factor of  
  • a binary resolvent of a factor of   and  
  • a binary resolvent of a factor of   and a factor of  


Example:

Given   and  .

A factor of   is  . A binary resolvent of   and   and hence also of   and   is  .

The following lemma is used in the completeness proof of resolution.

Lemma 5 (Lifting lemma) edit

If   and   are instances of   and  , respectively, and   is a resolvent of   and  , then there is a resolvent   of   and   such that   is an instance of  .

 
Figure 1

Theorem 8 edit

A set   of clauses is unsatisfiable iff the empty clause can be derived from   by resolution.
Proof:
Assume that   is unsatisfiable. Let   be the ground atom set of  , hence the Herbrand basis. Let   be a complete binary tree, as given in Figure 2. According to Herbrand's theorem (version1) there exists a closed finite semantic tree  . There are two cases:

  • If   consists only of one node (hence the root), The interpretation to be collected from the empty branch in this tree falsifies only the empty clause. Hence the empty clause must be in  .
  • Assume   consists of more than one node. Then there must be an inference node   in  , hence both its descendants   and   are failure nodes. If such a node would not exist, every node would have at least one non-failure node, which would mean that there is at least an infinite path in  , which would violate, that fact that it is a finite closed semantic tree. Let   given as described above; and let
     

Now, let   and   be ground instances of clauses   and  , such that   is falsified by   and   by  , such that both are not falsified by  .

Hence we have   and   and we can construct the resolvent

 

  must be false in  , because both   and   are false in  . According to the Lifting Lemma 5 there exists a resolvent   of   and  , such that   is a ground instance of  . Let   be the closed semantic tree for   , obtained from   by deleting all nodes below the first node which falsifies  . Note, that   is unsatisfiable if and only if   is unsatisfiable. Clearly,   has less nodes than   and we now can iterate this process until only the root of the semantic tree is remaining. This, however is only possible if the empty clause   is derivable. For the opposite direction, assume that   is derivable by resolution from   and let   the resolvents constructed during this process. Assume   is satisfiable and   to be a model for  . From the correctness lemma according to the propositional case we known, that if a model satisfies two clauses it also satisfies its resolvent. Therefore   has to satisfy  ; this, however, is impossible, because one of this resolvents is  .


 


Figure 2

Problems edit

Problem 14 (Predicate) edit

Indicate in each case a derivation of the empty clause with predicate-logical resolution!

  1.  
  2.  
    ( )
  3.  


 

Problem 15 (Predicate) edit

Show the following Lifting lemma by means of induction over the term- and formula construction: Is   a predicate-logical formula, and   a fitting interpretation for

  and  . Then

 


is valid, if   does not contain any variable that   is laced

by the substitution in  .
 

Problem 16 (Predicate) edit

Compute - if possible - the most general unifier of following sets of clauses:

  1.  
  2.  
  3.  
  4.  


 

Problem 17 (Predicate) edit

Determine all direct resolvents of the following pairs of clauses:

  1.   and  
  2.   and  
  3.   and  
  4.   and  


 

Problem 18 (Predicate) edit

Compute - if possible - the most general unifier of following sets of clauses:

  1.  
  2.  
  3.  
  4.  


 

Problem 19 (Predicate) edit

Determine all direct resolvents of the following pairs of clauses:

  1.   and  
  2.   and  
  3.   and  


 

Problem 20 (Predicate) edit

Give for the following set of clauses (a) a linear derivation, (b) a derivation with unit resolution, (c) a further (maximally short) derivation of the empty clause by means of predicate-logical resolution!

 


 

Problem 21 (Predicate) edit

Indicate in each case a derivation of the empty clause with predicate-logical resolution!

  1.  
  2.  
    ( )
  3.