Источник: Department of Computer Science
Resolution for Predicate Logic
The connection between general satisfiability and Her- brand satisfiability provides the basis for a refutational approach to first-order theorem proving.
Validity of a first-order sentence φ can be checked as follows.
1. First convert the negated formula ¬φ into a prenex form Q1x1 . . . Qnxn ψ.
2. Next skolemize to obtain a universal formula of the form ∀x1 . . . ∀xn ψt.
3. Then convert ψt into conjunctive form, ψ ∧ . . . ∧ ψ, where each formula ψ is a disjunction of literals. The formula ∀x1 . . . ∀xn ψt is equivalent to
(∀x1 . . . ∀xn ψ1) ∧ . . . ∧ (∀x1 . . . ∀xn ψm).
4. Finally, apply suitable “resolution” inferences to
ψ1, . . . , ψm,
interpreting each formula ψ as a clause.
If a contradiction is derived, then ¬φ is unsatisfiable, which implies that φ is valid.
Renaming
A substitution is said to be a renaming if it is a one-to- one and onto function on the set of variables.
For example, the substitution
σ = [x '→ y, y '→ x]
is a renaming (in this case of the variables x and y).
We also call a substitution ρ a renaming for a formula φ if ρ(x) and ρ(y) are different variables, whenever x and y are different variables in φ.
If C is a clause and ρ a renaming for C , then C and C ρ obviously have the same ground instances. Thus the Herbrand semantics of a clause does not change under renaming.
We will employ renaming substitutions, as well as (most general) unifiers, in defining inferences on clauses.
Binary Resolution
The following inference rule provides a strating point for a refutational theorem proving method for clauses.
C ∨ A D ∨ ¬B C ρσ ∨ Dσ
where ρ is a renaming substitution, such that the re- named first premise has no variables in common with the second premise, and σ is a most general unifier of Aρ and B.
For example,
P (f x, x) ¬P (x, f y) ∨ ¬P (x, z)
¬P (f f y, z)
is a binary resolution inference.
Example – Resolution
Consider the set of the following clauses:
¬P (x, y) ∨ P (y, x) (1)
¬P (x, y) ∨ ¬P (y, z) ∨ P (x, z) (2)
P (x, f x) (3)
¬P (a, a) (4)
We use resolution to show that this set is unsatisfiable. From clauses (3) and (1) we obtain
P (f x1, x1) (5)
whereas from (3) and (2) we get
¬P (f x2, z) ∨ P (x2, z) (6) Resolving clauses (5) and (6) yields
P (x3, x3) (7)
which can be resolved with (4) to yield a contradiction.
Factoring
Binary resolution by itself is not sufficient to obtain a contradiction from every unsatisfiable set of clauses, but needs to be supplemented by the following rule.
C ∨ A ∨ B C σ ∨ Aσ
if σ is a most general unifier of the positive literals A
and B.
The following inference rule is not necessary (for refu- tational completeness), but can also be used.
C ∨ ¬A ∨ ¬B C σ ∨ ¬Aσ
if σ is a most general unifier of A and B.
Resolution
Factoring can also be integrated into resolution infer- ences.
C ∨ A1 ∨ · · · ∨ Ak D ∨ ¬B1 ∨ · · · ∨ ¬Bl
C ρσ ∨ Dσ
where ρ is a renaming substitution for the first premise such that the renamed clause has no variables in com- mon with the second premise, and σ is a most general
unifier of {A1ρ, . . . , Akρ, B1, . . . , Bl}.
For example,
R(f f x, x) ¬R(y, z) ∨ R(f y, f z)
R(f f f x, f x)
is a resolution inference. In this example, no renaming is necessary (and hence ρ may be the identity function) and the atoms to be unified are R(f f x, x) and R(y, z),
which have most general unifier σ = [y '→ f f x, z '→ x].
Another Example
Recursively define terms f n(x) by: (i) f 1(x) = f (x) and
(ii) f n(x) = f (f n−1(x)), if n > 1.
Let Sn denote the set of two clauses,
P (x) ∨ P (f (x))
¬P (y) ∨ ¬P (f n(y))
For example, S1 consists of these clauses:
P (x) ∨ P (f (x))
¬P (y) ∨ ¬P (f y)
This set is satisfiable, as there is a Herbrand interpre- tation in which all ground instances of both clauses are true.
(Consider a language with a single constant a. Then the Herbrand universe consists of the terms
a, f a, f f a, . . .
Define P I in such a way that P I (t) is true if, and only if, t is a term f n(a), for which n is an odd number. This Herbrand model I satisfies S1.)
Example (cont.)
Next take the set S2:
P (x) ∨ P (f (x)) (1)
¬P (y) ∨ ¬P (f y) (2)
Resolving (1) and (2) yields
¬P (x) ∨ P (f (x)) (3) From (3) and (2) we obtain
¬P (x) ∨ ¬P (f (x)) (4)
Resolving (3) and (4) yields
¬P (x) ∨ ¬P (x) (5) From (1) and (5) we obtain
P (x) (6)
Clauses (5) and (6) yield a contradiction, which implies that the set S2 is unsatisfiable.
(Resolvents have been consistently renamed so as to simplify the presentation.)
Example (cont.)
The set S6, it turns out, is also unsatisfiable. Here is a refutation by resolution.
P (x) ∨ P (f (x)) (1)
¬P (x) ∨ ¬P (f 6(x)) (2)
¬P (x) ∨ P (f 5(x)) (1), (2) : (3)
¬P (x) ∨ ¬P (f (x)) (2), (3) : (4)
¬P (x) ∨ P (x) (1), (4) : (5)
¬P (x) ∨ ¬P (f 4(x)) (3), (4) : (6)
¬P (x) ∨ P (f 3(x)) (1), (6) : (7)
¬P (x) ∨ ¬P (f (x)) (3), (6) : (8)
¬P (x) ∨ ¬P (f 3(x)) (2), (7) : (9)
¬P (x) ∨ ¬P (f 2(x)) (4), (7) : (10)
¬P (x) ∨ ¬P (f (x)) (6), (7) : (11)
¬P (x) ∨ P (f 2(x)) (1), (9) : (12)
¬P (x) ∨ ¬P (f 2(x)) (3), (9) : (13)
¬P (x) (7), (9) : (14)
P (x) (1), (14) : (15)
⊥ (14), (15) : (16)
Soundness of Resolution
The inferences we have described above–binary and gen- eral resolution and factoring—are logically sound.
Theorem [Soundness]
The conclusion of a resolution or factoring in- ference is true in every Herbrand model that satisfies the premises of the inference.
Instances of Inferences
An instance of a resolution inference
C D C tρσ ∨ Dtσ
is any inference
C ρστ Dστ
C tρστ ∨ Dtστ
Similarly, by an instance of a factoring inference
C ∨ L ∨ Lt
C σ ∨ Lσ
we mean any inference
C στ ∨ Lστ ∨ Ltστ
C στ ∨ Lστ
If neither premises nor conclusion contain any variables, we speak of a ground instance.
Note that instances of a resolution inference need not themselves be resolution inferences (as inferences em- ploy only most general unifiers).
Projection
The connection between (a) ground instances of infer- ences from arbitrary clauses and (b) inferences from ground instances of clauses, forms the basis of the refu- tational completeness of resolution plus factoring.
Let C and D be two clauses with no variables in common and C τ and Dτ be corresponding ground instances.
(i) If Et is the conclusion of a resolution infer- ence with premises C τ and Dτ , then Et is a
ground instance of a clause E that is the con- clusion of a resolution inference with premises C and D.
(ii) If Et is the conclusion of a factoring in- ference with premise C τ , then Et is a ground
instance of a clause E that is the conclusion of a factoring inference with premise C .
Refutational Completeness
A set of clauses N is saturated (with respect to given inference rules) if N contains the conclusion of every inference, the premises of which are elements of N .
The following lemma follows from the Lifting Lemma.
If a set of clauses N is saturated with respect to resolution and factoring, then the set of all ground instances of clauses in N is saturated with respect to ground resolution and factor- ing.
Observing that the empty clause is an instance of itself, but of no other clause, we obtain:
A set of clauses is unsatisfiable if and only if the empty clause can be derived from it by resolution and factoring.
Subsumption
Some clauses may be redundant in the sense that they are not needed for deriving a contradiction.
We say that a clause C subsumes another clause D if D
can be written as C σ or C σ ∨ C t, for same substitution
σ.
For example, the ground clause P ∨ Q subsumes P ∨ Q ∨
¬R, and P (x) subsumes P (f (y)) ∨ Q(y).
A clause C is redundant with respect to a set N if N contains a(nother) clause that subsumes C . Redundant clauses may be ignored in derivations.