Logic for Computer Scientists/Predicate Logic/Resolution
Resolution[edit | edit source]
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 | edit source]
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 | edit source]
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 | edit source]
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 | edit source]
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.
Given a set of expression. Transform it into a set of equations
as defined above. Apply the following transformation rules as long as
possible:
- Orient
where is a variable and a non-variable term - Delete
- Decompose (Termreduction)
- Eliminate (Elimination of variable I)
if not in , but in
- Coalesce (Elimination of variable II)
if in - Conflict
if or
- Occur Check
if in
Theorem 7[edit | edit source]
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 | edit source]
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 | edit source]
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 | edit source]
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 | edit source]
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 .
Theorem 8[edit | edit source]
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 .
Problems[edit | edit source]
Problem 14 (Predicate)[edit | edit source]
Indicate in each case a derivation of the empty clause with predicate-logical resolution!
- ()
Problem 15 (Predicate)[edit | edit source]
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 | edit source]
Compute - if possible - the most general unifier of following sets of clauses:
Problem 17 (Predicate)[edit | edit source]
Determine all direct resolvents of the following pairs of clauses:
- and
- and
- and
- and
Problem 18 (Predicate)[edit | edit source]
Compute - if possible - the most general unifier of following sets of clauses:
Problem 19 (Predicate)[edit | edit source]
Determine all direct resolvents of the following pairs of clauses:
- and
- and
- and
Problem 20 (Predicate)[edit | edit source]
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 | edit source]
Indicate in each case a derivation of the empty clause with predicate-logical resolution!
- ()