First Order Logic: First-order resolution.

V Goranko

First Order Logic:

First-order resolution.

Valentin Goranko DTU Informatics

September 2010

V Goranko

First-order resolution

The Propositional Resolution rule extended to first-order logic:

C ∨Q(s₁, . . . ,s_n), D∨ ¬Q(s₁, . . . ,s_n) C ∨D

This rule, however, is not strong enough.

Example: the clause set

{{P(x)},{¬P(f(y))}}

is not satisfiable, as it corresponds to the unsatisfiable formula

∀x∀y(P(x)∧ ¬P(f(y))).

However, the resolution rule above cannot derive an empty clause from that clause set, because itcannot unify the two clauses in order to resolve them.

So, we need a stronger resolution rule.

V Goranko

Two solutions

Solution 1: Ground resolution: generate sufficiently manyground instancesof every clause over aHerbrand universeof the language.

In the example, ground resolution would generate the ground clauses{P(f(c))} and{¬P(f(c))} for some constant symbolc. This method is sound and complete but inefficient, as it leads to the generation of too many unnecessary clauses.

Ground resolution was introduced in:

John Alan Robinson: A Machine-Oriented Logic Based on the Resolution Principle, JACM, 1965.

Will not be discussed further.

Solution 2: Resolution with unification.

V Goranko

Substitutions of terms for variables revisited

s[t/x]is the result of simultaneousreplacements of all occurrences ofx ins byt. For instance:

f(g(x),f(y,x)) [g(a)/x] =f(g(g(a)),f(y,g(a))).

This can generalize to simultaneous substitutions of several terms fordifferent variables, denoted s[t1/x1, . . . ,t_k/x_k]. For instance:

f(g(x),f(y,x)) [g(y)/x,f(x,b)/y] =f(g(g(y)),f(f(x,b),g(y))).

Given the substitutionσ= [t1/x1, . . . ,tk/xk], the set of variables {x₁, . . . ,x_k} is called the domainof σ.

Simultaneity is important: if we first substitutedg(y) forx and thenf(x,b) fory the result would have been different (and wrong).

Substitution in a literal is a substitution in all of it argument terms simultaneously. For instance:

P(x,f(x,y),g(y)) [g(y)/x,a/y] =P(g(y),f(g(y),a),g(a)).

V Goranko

Composition of substitutions

Substitutions can be composed by consecutive application:

the composition of substitutionsτ andσ is a substitutionτ σ obtained by applyingτ followed by applying σ to the result, i.e., tτ σ = (tτ)σ (note the order). For instance:

f(g(x),f(y,x)) [f(x,y)/x][g(a)/x,x/y] = f(g(f(x,y)),f(y,f(x,y))) [g(a)/x,x/y] =

f(g(f(g(a),x)),f(x,f(g(a),x))).

V Goranko

Computing the composition of substitutions

The composition of two substitutionsτ = [t₁/x₁, . . . ,t_k/x_k] andσ can be computed as follows:

1. Extend dom(τ) to cover dom(σ) by adding toτ substitutions [x/x] for every variablex in dom(σ)\dom(τ).

2. Apply the substitution σ simultaneously to all terms [t₁, . . . ,t_k] to obtain the substitution [t₁σ/x₁, . . . ,t_kσ/x_k].

3. Remove from the result all casesx_i/x_i, if any.

Example:

[f(x,y)/x,x/y][y/x,a/y,g(y)/z] = [f(x,y)/x,x/y,z/z][y/x,a/y,g(y)/z]

= [f(y,a)/x,y/y,g(y)/z]

= [f(y,a)/x,g(y)/z] .

V Goranko

Unification of terms

A substitutionσ that makes two termss andt identical is called a unifier ofs andt. Examples:

• the substitution [f(y)/x] unifies the terms x and f(y);

• the substitution [f(c)/x,c/y,c/z] unifies the terms g(x,f(f(z))) and g(f(y),f(x)).

• There is no unifier for the pair of termsf(x) andg(y), nor for the pair of terms f(x) andx.

V Goranko

Unification of atomic formulae

A substitutionσ that makes the (respective arguments of the) atomic formulaeQ(s₁, . . . ,s_n) andQ(t₁, . . . ,t_n) identical is called aunifier ofQ(s₁, . . . ,s_n) andQ(t₁, . . . ,t_n). Examples:

• [f(y)/x] unifies P(x) andP(f(y));

• [f(c)/x,c/y,c/z] unifies Q(x,c,f(f(z))) and Q(f(y),z,f(x)).

Indeed, the results of applying the substitutionσ are:

Q(x,c,f(f(z)))σ=Q(f(c),c,f(f(c))), Q(f(y),z,f(x))σ =Q(f(c),c,f(f(c))).

V Goranko

Most general unifiers

A unifierτ of two terms (or, atomic formulae) ismore general than a unifierρ, if ρ=τ σ, whereσ is some substitution and τ σ is the composition ofσ with τ (i.e,σ applied after τ).

Remark: Every unifier is ’more general’ than itself.

Better terminology: ’at least as general’.

Example: ρ= [c/x,f(c)/y] is a unifier of the literals P(f(x)) and P(y), but τ = [f(x)/y] is amore general unifierthanρ, because ρ=τ σ, whereσ= [c/x].

A unifier of two terms is theirmost general unifier (MGU)if it is more general than any unifier of theirs.

Likewise for atomic formulae.

If two terms (or, atomic formulae) are unifiable then they have a most general unifier. However, it need not be unique.

In the example above,τ is a most general unifier, as well as the unifier [z/x,f(z)/y] for any variablez.

V Goranko

Computing a most general unifier of list of terms

In order to unify two literalsQ(s1, . . . ,sn) and Q(t1, . . . ,tn), we must unify their respective pairs of arguments, i.e., we are looking for a (most general) unifier of the system:

t₁ =s₁, ... tn=sn.

Informally, we do that by computing a most general unifier (if one exists) of the first pair, then applying it to both lists of terms, then computing a most general unifier of the next pair (if there is one) in the resulting lists, applying it to the resulting lists of terms, etc.

In order to unify the current pair of terms we apply the algorithm recursively to the pair of lists of their respective arguments.

The composition of all most general unifiers computed as above, if they all exist, is a most general unifier of the two input lists.

V Goranko

Algorithm for computing most general unifiers

procedure mgu(p, q)

θ := ε (the empty substitution).

Scan p and q simultaneously, left-to-right,

and search for the first corresponding subterms where p and q disagree (mismatch).

If there is no mismatch, return θ.

Else, let s and t be the first respective subterms in p and q where mismatch occurs.

If variable(s) and s ∈/ Var(t) then θ := compose(θ,[t/s]);

θ := compose(θ, mgu(pθ,qθ)).

Else, if variable(t) and t ∈/ Var(s) then θ := compose(θ,[s/t]);

θ := compose(θ, mgu(pθ,qθ)).

Else, return failure.

end

V Goranko

Examples of computing most general unifiers

1. Literal 1: parents(x, father(x), mother(Bill)), Literal 2: parents(Bill, father(Bill), y), MGU: [Bill/x, mother(Bill)/y].

2. Literal 1: parents(x, father(x), mother(Bill)).

Literal 2: parents(Bill, father(y), z).

MGU: [Bill/x, Bill/y, mother(Bill)/z].

3. Literal 1: parents(x, father(x), mother(Jane)).

Literal 2: parents(Bill, father(y), mother(y)).

MGU: [Bill/x, Bill/y, ...failure].

Therefore, MGU does not exist.

4. Term 1: g(x,f(x)).

Term 2: g(f(y),y).

MGU: [f(y)/x, . . . failure]. MGU does not exist.

V Goranko

First-order resolution with unification

The first-order Resolution rule is combined with a preceding unification of the clausal set, in order to produce a complementary pair of literals in the resolving clauses:

Res: C ∨Q(s1, . . . ,sn), D∨ ¬Q(t₁, . . . ,tn) (C ∨D)σ

where:

(i) the two clauses have no variables in common (achieved by renaming of variables, if necessary), and

(ii)σ is an MGU of the literalsQ(s₁, . . . ,s_n) andQ(t₁, . . . ,t_n).

We require that the unifier applied in the rule is a most general unifier of the respective literals in order not to weaken the resolvent unnecessarily.

V Goranko

First-order resolution with unification:

some examples of applications of the rule

{P(x)},{¬P(f(y))}

{} (MGU : [f(y)/x])

{P(a,y), Q(y)}{¬P(x,b),Q(x)}

{Q(b),Q(a)} (MGU : [a/x,b/y]) {P(a,y), Q(y)}{¬P(x,f(x)), Q(f(x))}

{Q(f(a))} (MGU : [a/x,f(a)/y])

Note that both literals in the resolvent become equal.

{P(a,y), P(x,f(x))}{¬P(x,f(a))}

{} (MGU : [a/x,f(a)/y]).

Note that, after unification, both literals in the first clause become P(a,f(a)).

V Goranko

Derivations with first-order resolution

Aresolution-based derivation of a formulaC from a list of

formulaeA1, . . . ,An, denotedA1, . . . ,An,`_ResC, is a derivation of the empty clause{} from the set of clauses obtained from

A₁, . . . ,A_n,¬C, by successive applications of the ruleRes.

Theorem: The method of First-order Resolution is sound and complete, i.e., for every first-order formulaeA1, . . . ,An,C:

A1, . . . ,An,`_ResC iff A1, . . . ,An,|=C.

However, unlike Propositional Resolution,First-order Resolution may run forever, i.e., never terminate, in some cases when the conclusion does not follow logically from the premises.

It may also run forever even when the conclusion follows logically from the premises, if unnecessary resolvents are produced.

To avoid that, special strategies or additional mechanisms for disposal of used-up clauses need to be applied.

V Goranko

First-order resolution:

factoring

• Factoring:

{. . .P(s),P(t). . .}

{. . .P(s). . .}σ , (σ=MGU(s,t))

• Example:

{P(x),P(c),¬Q(x,y)}

{P(c),¬Q(c,y)} (MGU : [c/x])

• Factoring is a sound rule. Some systems of FOL resolution employ it together with the rule Res.

V Goranko

First-order resolution with unification:

Example 1

Prove with the method of First-order resolution that:

∀x(P(x)→Q(x))|=∀xP(x)→ ∀xQ(x) :

1. Transform

{∀x(P(x)→Q(x)),¬(∀xP(x)→ ∀xQ(x))}

to clausal form:

{¬P(x),Q(x)}, {P(y)}, {¬Q(c)}

for some Skolem constantc. 2. Successive applications of Res:

2.1 UnifyP(x) andP(y) with MGU [y/x].

Then resolve{¬P(y),Q(y)}and{P(y)} to obtain{Q(y)}.

2.2 UnifyQ(c) andQ(y) with MGU [c/y].

Then resolve{¬Q(c)} and{Q(c)} to obtain{}.

V Goranko

First-order resolution with unification:

Example 2

Prove that:

If Everybody loves somebody andEverybody loves every lover thenEverybody loves everybody.

1. Formalize the assumptions and the goal conclusion, using the predicateL(x,y) meaning ‘x lovesy’:

Everybody loves somebody: ∀x∃yL(x,y).

Everybody loves every lover: ∀x(∃yL(x,y)→ ∀zL(z,x)).

Everybody loves everybody: ∀x∀yL(x,y).

2. Transform the set

{∀x∃yL(x,y), ∀x(∃yL(x,y)→ ∀zL(z,x)), ¬(∀x∀yL(x,y))}

to clausal form:

{L(x,f(x))}, {¬L(x₁,y),L(z,x₁)}, {¬L(a,b)}, for some Skolem constants a,b and a Skolem functionf.

V Goranko

Now, applyResrepeatedly to the resulting set of clauses {L(x,f(x))}, {¬L(x₁,y),L(z,x1)}, {¬L(a,b)}:

1. Unify L(z,x₁) andL(a,b) with MGU [b/x₁,a/z] and resolve {¬L(b,y),L(a,b)}and{¬L(a,b)} to obtain {¬L(b,y)}.

2. Unify L(x,f(x)) and L(b,y) with MGU [b/x,f(b)/y] and resolve {L(b,f(b))} and{¬L(b,f(b))} to obtain {}.

V Goranko

First-order resolution with unification:

Example 3

Check if

∀x∃yR(x,y),∀x∀y∀z((R(x,y)∧R(y,z))→R(x,z))|=∃xR(x,x) :

Transform

{∀x∃yR(x,y),∀x∀y∀z((R(x,y)∧R(y,z))→R(x,z)),¬(∃xR(x,x))}

to clausal form:

C₁ ={R(x,f(x))},C₂ ={¬R(u,y),¬R(y,z),R(u,z)},C₃ ={¬R(v,v)}

for some unary Skolem functionf.

V Goranko

Successive applications of Res to the clausal set

C1 ={R(x,f(x))},C2 ={¬R(u,y),¬R(y,z),R(u,z)},C3 ={¬R(v,v)}

1. UnifyR(u,z) in C₂ andC₃, with MGU [v/u,v/z] and resolve:

C4 ={¬R(v,y),¬R(y,v)}.

2. UnifyR(v,y) in C₄ andC₁ with MGU [w/x,w/y,f(w)/v] and resolve: C5 ={¬R(f(w),w)}.

3. UnifyR(u,z) in C₂ andC₅ with MGU [f(w)/u,w/z] and resolve: C6 ={¬R(f(w),y),¬R(y,f(w))}.

4. UnifyR(f(w),y) in C6 andC1 with MGU [f(w)/x,f(f(f(w))/y] and resolve:

C₇ ={¬R(f(f(w)),f(w))}, etc.

Thus, an infinite set of clauses can be generated:

{¬R(f(w),w)},{¬R(f(f(w)),f(w))},{¬R(f(f(f(w))),f(f(w)))}, . . . but the empty clause cannot be derived.

In fact, the logical consequence does not hold. A countermodel is the set of natural numbers withR(x,y) interpreted asx <y.