Transcript A A S x

General Resolution
method in FOL
Lesson 8
7. 4. 2016
General resolution Method
1
Typical problems to solve
 Proving logical validity of a formula:

Formula F is logically valid, denoted |= F, iff F is true
in all interpretations, i.e., every interpretation structure
is its model
 Proving the validity of an argument:

An argument is valid, denoted P1, …, Pn |= Q, iff the
formula Q is true in all the models of the set of
assumptions P1, …, Pn
 What follows from the assumptions?

7. 4. 2016
P1, …, Pn |= ?
General resolution Method
2
Typical problems, tasks
 Their solution by examining the infinite set of models is difficult; it is not




possible to automatize semantic proofs
Therefore we look for syntactic (mechanic) methods of proving
One of them is the method of semantic tableau based on the
transformation of a formula into its disjunctive normal form
(disadvantage: we often need to perform many transformations using
the distributive laws)
Now we are going to learn a very effective method that is used also for
automatic theorem proving and programming in logic: the resolution
method for FOL (generalization of the resolution method for
propositional logic)
Rezolution method makes use of the conjunctive normal form of a
formula
7. 4. 2016
General resolution Method
3
Resolution method
 It
is applicable to a formula in the
special kind of the conjunctive normal
form: Skolem clausal form
 It makes use of the indirect proof
 It serves as a theoretical foundation for
automatic theorem proving and logic
programming;
 In particular for the programming
language PROLOG
7. 4. 2016
General resolution Method
4
Resolution method
In order to generalize the resolution method of
propositional logic, there are two problems:
1)
Transformation into the Skolem clausal form:
x1…xn [C1  …  Cm]
where Ci are clauses, i.e., disjunctions of literals,
e.g.: P(x)  Q(f(x,y))
2)
In order to apply the resolution rule on a pair of a
positive and negative literals, the literals have to
be identical; we have to unify them.
For instance: P(x)  Q(f(x),y)
P(g(y))  Q(x,z)
The literals P(x), P(g(y)) might have been
eliminated, if they were identical; we have to unify
them by substituting g(y) for x.
7. 4. 2016
General resolution Method
5
Transformation into the clausal form
(Skolem)
1.
2.
3.
4.
5.
6.
7.
8.
9.
Existential generalization (if there are free varaibles,
then bind them by  (consistency preserving)
Elimination of dispensable quantifiers
Elimination of the connectives , 
Moving negation inside (applying de Morgan laws)
Renaming variables
Moving quantifiers to the right
Elimination of existential quantifiers
(Skolemization – consistency preserving)
Moving general quantifiers to the left
Applying distributive laws
7. 4. 2016
General resolution Method
6
Resolution method – example.
|= [x y P(x,y)  y z Q(y,z)]  x y z [P(x,y)  Q(y,z)]
1. Negating the formula and variables renaming:
[x y’ P(x,y’)  y z Q(y,z)]  u v w [P(u,v)  Q(v,w)]
2. Elimination of existential quantifiers.
MIND !
[x P(x, f(x))  y Q(y, g(y))]  v w [P(a,v)  Q(v,w)]
3. Moving the quantifiers to the left:
x y v w [P(x, f(x))  Q(y, g(y))  [P(a,v)  Q(v,w)]]
4. The formula is obviously not satisfiable; how to prove it?
5. Write down the clauses and perform the unification of
literals, i.e., substitute appropriate terms for variables,
so that to be able to apply the resolution rule:
7. 4. 2016
General resolution Method
7
Resolution method – example
1.
2.
3.

4.
5.
P(x, f(x))
Q(y, g(y))
P(a,v)  Q(v,w)
Now we have to apply resolution rule. In order to resolve
clauses 1. and 3., we have to substitute the term a for the
variable x and the term f(a) for variable v.
Q(f(a),w)
resolving 1., 3., substitution: x/a, v/f(a)
resolving 2., 4., substitution: y/f(a), w/g(f(a))
QED – the negated formula is a contradiction, which means that
the original formula is logically valid
Note: When unifying the literals, it is necessary to substitute for
all the occurrences of a variable!
7. 4. 2016
General resolution Method
8
Skolem clausal form
Literal: atomic formula or the negation of an atomic formula.
Examples: P(x, g(y)), Q(z)
Clause: disjunction of literals, e.g.: P(x, g(y))  Q(z)
Skolem clausal form: x1…xn [C1  …  Cm],
a closed formula, where Ci are clauses, disjunctions of
literals, e.g.: P(x)  Q(f(x,y))
Skolemization (elimination of existential quantifiers):
x y1...yn A(x, y1,...,yn)  y1...yn A(c, y1,...,yn)
where c is a new, in the language not used constant
y1...yn x A(x, y1,...,yn)  y1...yn A(f(y1,...,yn), y1,...,yn)
where f is a new, in the language not used functional
symbol
7. 4. 2016
General resolution Method
9
Skolemization is consistency preserving
y1...yn x A(x, y1,...,yn)  y1...yn A(f(y1,...,yn), y1,...,yn)
BS
B

Proof: Let the structure I be a model of the formula BS (Skolemised).
Then for any n-tuple of individuals i1, i2,…,in it holds that (n+1)-tuple of
individuals i1, i2,…,in, fU (i1, i2,…,in)  AU, where fU is the function
assigned to the symbol f (in the interpretation I) and AU is the relation
defined by the formula A in the interpretation I. Then the interpretation
structure I is also a model of the formula B =
y1y2…yn x A(x, y1, y2,…,yn).

Hence every model of the formula BS is a model of the formula B, but not
vice versa, ie BS |= B.

The set of models MBS of the formula BS is a subset of the set of models
MB of the formula B: MBS  MB.

If MBS   (i.e., BS is satisfiable) then MB  , i.e., B is satisfiable as well.

If MB = , i.e. B is not satisfiable, then MBS = , i.e., BS is not satisfiable,
which is sufficient for the indirect proof.
7. 4. 2016
General resolution Method
10
Thoralf Albert Skolem
Born: 23 May 1887 in Sandsvaer, Buskerud, Norway
Died: 23 March 1963 in Oslo, Norway
Skolem was remarkably
productive publishing
around 180 papers on
topics such as
Diophantine equations,
mathematical logic,
group theory, lattice
theory and set theory
7. 4. 2016
General resolution Method
11
Transformation into the Skolem clausal form
A  AS:
1.
Existential generalization (consistency preserving)
2.
Elimination of dispensable quantifiers (that do not bind any variables –
equivalent transformation)
3.
Elimination of ,  (applying the PL laws – equivalent transformation)
4.
Moving negation inside (applying de Morgan laws – equivalent
transformation)
5.
Renaming variables (equivalent transformation)
6.
Moving quantifiers to the right (equivalent transformation):
Qx (A @ B(x))  A @ Qx B(x),
Qx (A(x) @ B)  Qx A(x) @ B,
where @ is a conjunction or disjunction connective,
Q is a quantifier (general or existential)
7.
Elimination of existential quantifiers
(Skolemize the subformulas Qx B(x), Qx A(x) obtain in the step 6)
8.
Moving general quantifiers to the left (equivalent transformation)
9.
Applying distributive laws (equivalent transformation)
7. 4. 2016
General resolution Method
12
Transforming A  AS (Skolem)


The resulting formula AS is not equivalent to the original
formula A (nor does it follow from A), but it holds that
if A has a model then AS has a model.
It also holds that AS |= A, but the two formulas are not
equivalent.
The non-equivalent steps are:




Existential generalisation
Skolemization (elimination of existential quantifiers)
This is the reason why the resolution method is used as an
indirect proof.
It can be used for a direct proof only if the assumptions do
not contain any existential quantifier
7. 4. 2016
General resolution Method
13
Transformation: A  AS



1.
2.
3.
4.
5.



Always follow the above Skolem algorithm (9 steps). Some of them can be omitted,
but do not transform into the conjunctive normal form first, and then Skolemize (as
you can sometimes read). In other words, do not omit the step 6.
Example: the importance of the step 6 (quantifiers to the right – moved to the
subformulas containing the quantified variables).
We will illustrate an erroneous practice of omitting the step 6 by (not) proving
that
|= x A(x)  x A(x):
negating the formula: x A(x)  x A(x),
Renaming variables: x A(x)  y A(y),
Moving quantifiers to the left:
x [A(x)  y A(y)]  x y [A(x)  A(y)], and
Skolemize: x [A(x)  A(f(x))].
But the terms x and f(x) cannot be unified! Thus we did not prove the above
tautology, though the resolution method is a complete proof method. Each logically
valid formula is provable:
|= A  | A
The problem consists in the fact that we Skolemized after moving quantifiers to the
left. We have to do it before, when the quantifiers are to the right – at the
subformulas that they actually quantify.
7. 4. 2016
General resolution Method
14
Example: A  AS
x {P(x)  z {y [Q(x,y)  P(f(x1))]  y [Q(x,y)  P(x)]}}
1.,2. Existential generalisation and elimination of z:
x1 x {P(x)  {y [Q(x,y)  P(f(x1))]  y [Q(x,y)  P(x)]}}
3.,4. Renaming y, elimination of :
x1 x {P(x)  {y [Q(x,y)  P(f(x1))]  z [Q(x,z)  P(x)]}}
5.,6. Negation moved inside, quantifiers to the right:
x1 x {P(x)  {[y Q(x,y)  P(f(x1))]  [z Q(x,z)  P(x)]}}
7. Elimination of the existential quantifiers:
x {P(x)  {[Q(x,g(x))  P(f(a))]  [z Q(x,z)  P(x)]}}
8. Quantifier z moved to the left:
x z {P(x)  {[Q(x,g(x))  P(f(a))]  [Q(x,z)  P(x)]}}
9. Distributive law:
x z {[P(x)  Q(x,g(x))]  [P(x)  P(f(a))]  [P(x)  Q(x,z)  P(x)]}
10. simplifying:
x {[P(x)  Q(x,g(x))]  [P(x)  P(f(a))]}
7. 4. 2016
General resolution Method
15
The way of proving by resolution

Proof of the logical validity of a formula A:
1.
2.
3.

Negate the formula A
Transform A into the clausal Skolem form (A)S
Step-by-step apply the resolution rule (via unifying the literals) and try
to prove that the formula (A)S is not satisfiable, hence also the
formula A does not have a model, which means that A is logically
valid.
Proof of the validity of an argument
P1,…,Pn | Z
1.
2.
3.
Negate Z
Transform the assumptions and the negated conclusion into the
Skolem clausal form
Step-by-step apply the resolution rule (via unifying the literals) and try
to prove the inconsistency of the set {P1,…,Pn, Z}
7. 4. 2016
General resolution Method
16
Unification of literals
Example:

x y z v [P(x, f(x))  Q(y, h(y))  (P(a, z)  Q(z, v))]

How to prove that the formula does not have a model?
1. P(x, f(x))
2. Q(y, h(y))
3. P(a, z)  Q(z, v)
Now if we want to resolve the respective clauses; but there
are no identical terms in the respective pairs of literals.
However, all the variables are bound by the general
quantifier. Hence we can apply the law of specialization, and
thus substitute terms for variables in order to find the
witness of inconsistency:
In order to unify literals of 1 and 3, we use the substitution
x/a, z/f(a).

7. 4. 2016
General resolution Method
17
Unification of literals




After substituting we obtain the following clauses:
1’.
P(a, f(a))
2.
Q(y, h(y))
3‘.
P(a, f(a))  Q(f(a), v)
Now resolving 1‘ and 3‘ we obtain:
4.
Q(f(a), v)
Now in order to resolve 2. and 4., we again use a substitution:
y/f(a), v/h(f(a))
and get
2‘.
Q(f(a), h(f(a)) )
4’.
Q(f(a), h(f(a)) )
5.
By resolving 2’, 4’ we obtain an empty clause that does not have a
model. Hence the original formula A does not have a model, it is a
contradiction.
7. 4. 2016
General resolution Method
18
Unification of literals
Up to now we sought particular substitutions in order to unify
literals ad hoc, intuitively looking for opposite “similar”
literals
We need to find an algorithm of unification.
There are many such algorithms, we will examine two of them:
a)
Herbrand procedure
b)
Robinson unification algorithm
Ad (a) A formula F is not satisfiable iff it is not true in any
interpretation structure, over any universe of discourse.
It might be useful to find just one universe such that F is a
contradiction iff F is not satisfiable over any interpretation
structure over this universe.
Is there any such universe? Yes, it was discovered by
Herbrand, and it is called Herbrand’s universe.
7. 4. 2016
General resolution Method
19
Jacques Herbrand
Born: 12 Feb 1908 in Paris, France
Died: 27 July 1931 in La Bérarde, Isère, France
École Normale Supérieure
at the age of 17 (!)
His doctoral thesis was
approved in April 1929
On a holiday in the Alps he
died in a mountaineering
accident at the age of 23
7. 4. 2016
General resolution Method
20
Herbrand procedure
Herbrand universe HF: consists of all the possible terms made
up from the constants and functional symbols occurring in
the formula; if there is no constant in the formula, then use
any constant.
Example:

For the formula A = x [P(a)  Q(b)  P(f(x))]
the HA = {a, b, f(a), f(b), f(f(a)), f(f(b)), …}

For the formula B = x y P( (f(x), y, g(x,y) )
the HB = {a, f(a), g(a,a), f(f(a)), g(a,f(a)), g(f(a),a), …}
Basic instances of a clause: all the variables are
substituted for by the elements of Herbrand universe
Theorem (Herbrand):
A formula A in the Skolem clausal form is not satisfiable iff
there is a finite conjunction of its basic instances that is not
satisfiable.
7. 4. 2016
General resolution Method
21
Herbrand procedure
Example:
1. P(x, f(x))
2. Q(y, h(y))
3. P(a, z)  Q(z, v)

Here the HA = {a, f(a), h(a), f(f(a)), f(h(a)), h(f(a)), h(h(a)), …}. Now
we create basic instances, substituting elements of (the ordered)
Herbrand universe for variables:
Substitution 1: {x/a, y/a, z/a, v/a}

P(a, f(a))  Q(a, h(a))  [P(a, a)  Q(a, a)]
Substitution 2: {x/a, y/a, z/a, v/f(a)}

P(a, f(a))  Q(a, h(a))  [P(a, a)  Q(a, f(a))]
etc., till we find
Substitution n: {x/a, y/f(a), z/f(a), v/h(f(a))}

P(a,f(a))  Q(f(a),h(f(a)))  [P(a,f(a))  Q(f(a),h(f(a)))]
Contradiction
7. 4. 2016
General resolution Method
22
Herbrand Procedure
Herbrand procedure is a method that partially decides
whether a given formula F is a contradiction; if F is a
contradiction then Herbrand procedure answers YES
after a finite number of steps, otherwise it may not
answer at all.
(One of the corollaries of Gödel’s theorem; there is no
procedure that would decide it totally.)
Problem: Space and time complexity of the algorithm; the
number of basic instances we need to generate till we
find the witness of contradiction is often to large to be
computationally tractable.
7. 4. 2016
General resolution Method
23
John Alan Robinson

In his 1965 article "A Machine-Oriented
Logic Based on the Resolution
Principle" John Alan Robinson laid an
important foundation for a whole branch of
automated deduction systems. The original
Prolog is essentially a refined automated
theorem prover based on Robinson's
resolution
7. 4. 2016
General resolution Method
24
Robinson’s algorithm (1965)



Let A be a formula containing variables xi, i=1,2,...,n. Let
us denote  ={x1/t1, x2/t2,...,xn/tn} the
simultaneous substitution of terms ti for all the
occurrences of variables xi for i=1,2,...,n. Then let A be
the formula that arises from A by performing the
substitution .
Unification (unification substitution) of formulas A, B is
the substitution  such that
A = B.
The general unification of formulas A, B is the
unification  such that any other unification  of formulas
A, B it holds that  =  (where   , it is not an empty
substitution);
in other words, the general unification leaves as much as
possible variables free.
7. 4. 2016
General resolution Method
25
Robinson’s algorithm (1965)
It is the algorithm of finding the general unification:

Assume that A = P(t1, t2,...,tn), B = P(s1,s2,...,sn),
where (for the sake of simplicity) at least one of the terms
ti, si is a variable.
1. For i = 1,2,...,n do:
a)
b)
c)
d)
2.
If ti = si then i =  (the empty substitution).
If ti  si then check whether the terms ti, si are such that one of them
is a variable, say x, and the other term, say r, does not contain this
variable x.
If Yes, then i = {x/r}.
If No, then finish the cycle: the formulas A, B are not unifiable.
If the cycle were not finished by the exception ad (d), then
A, B are unifiable, and the general unification  =
12...n (the composed substitution).
7. 4. 2016
General resolution Method
26
Robinson’s algorithm
Example: A = Px, f(x), u, B = Py, z, g(x,y)
 1 = {x/y},
A1 = P(y, f(y), u, B1 = Py, z, g(y,y)
 2 = {z/f(y)},
A12 = P(y, f(y), u, B12 = Py, f(y), g(y,y)
 3 = {u/g(y,y)},
A123 = P(y, f(y), g(y,y),
B123 = Py, f(y), g(y,y).
 The composed substitution =123 is the general
unification of the formulas A, B:
{x/y, z/f(y), u/g(y,y)}
7. 4. 2016
General resolution Method
27
General resolution rule
A  L1, B  L2

A  B
where  is the general unification of L1, L2:
L1 = L2
7. 4. 2016
General resolution Method
28
Example: prove the logical validity of
xy [{P(x,y)  Q(x, f(g(x)))} 
{R(x)  x Q(x, f(g(x)))}  x R(x)]  x P(x, g(x))
1. Negate the formula:
xy [{P(x,y)  Q(x, f(g(x)))} 
{R(x)  x Q(x, f(g(x)))}  x R(x)]  x P(x, g(x))
2. Eliminate existential quantifiers, and rename the variables:
xy [{P(x,y)  Q(x, f(g(x)))} 
{R(x)  Q(a, f(g(a)))}  R(b)]  z P(z, g(z))
3. Write down the clauses (after eliminating the implication):
7. 4. 2016
General resolution Method
29
Example
xy [{P(x,y)  Q(x, f(g(x)))} 
{R(x)  Q(a, f(g(a)))}  R(b)]  z P(z, g(z))
1.
2.
3.
4.
5.
6.
7.
P(x,y)  Q(x, f(g(x)))
R(x)  Q(a, f(g(a)))
R(b)
P(z, g(z))
Q(x, f(g(x)))
1, 4:
Q(a, f(g(a)))
2, 3:
5, 6:
z/x, y/g(x)
x/b
x/a
Note: Parent clauses to resolve are chosen in such a way
that leaves as much as possible variables free (for
further substitutions)
7. 4. 2016
General resolution Method
30