Transcript Constraint propagation

AR: clausal logic
The step to Resolution
A deeper study:
Ground Horn Logic
Horn Logic
Clausal Logic
Modus ponens
Unification
Resolution
Representation-power
of Horn clauses
 Most predicate logic formulae can easily be
rewritten in Horn clauses.
 Examples:
x cat(x)  dog(x)  pet(x)
x poodle(x)  dog(x)  small(x)
pet(x)  cat(x)
pet(x)  dog(x)
dog(x)  poodle(x)
small(x)  poodle(x)
 BUT:
x human(x)  male(x)  female(x)
????
x dog(x)  ~abnormal(x)  has_4_legs(x)
????
3
Clausal form
 Generalized form of the formulae:
x1 … xk
A1  A2 …  Am  B1  B2 …  Bn
 Horn clauses are a special case with m = 1
 We assume that S = T  {~F} consists only of
clausal formulae.
 Goal: prove that S is inconsistent.
4
Example: Moore’s problem
 Given 3 blocks:
Blue or Red
 Prove that there is a blue block next to a red block!
5
Moore’s problem (2):
 In clausal form:
blue(Block1)
red(Block3)
blue(Block2)  red(Block2)
next_to(Block1,Block2)
next_to(Block2,Block1)
next_to(Block2,Block3)
next_to(Block3,Block2)
 Prove: b1 b2 next_to(b1,b2)  blue(b1)  red(b2)
or false  next_to(b1,b2)  blue(b1)  red(b2)
is inconsistent.
 PROBLEM: Modus ponens is not suitable for
blue(Block2)  red(Block2)
This would require a case-analysis!
6
Introducing negation in
bodies is equivalent:
 Example:
high_qualified(x)  phd(x)
earn_early(x)  ~phd(x)
rich(x)  high_qualified(x)
rich(x)  earn_early(x)
(1)
(2)
(3)
(4)
 Prove: rich(I)
 Why equivalent?
 (2) is equivalent to earn_early(x)  phd(x) since
A  ~B  A  B
7
Disjunction versus negation
in general:
x1 … xk
A1  A2 …  Am  B1  B2 …  Bn
is equivalent to:
x1 … xk
A1  B1  B2 …  Bn  ~A2  …  ~Am
or to:
x1 … xk
Ai  B1  B2 …  Bn  ~A1 .. ..  ~Am
~B 
A
A
 BB and basic relations
 Proof: AA  ~B
between ,  and ~
8
The resolution principle
 Propositional case:
A1  A2  …  Am  B1  …  B  …  Bn
C1  ...  B  …  Ck  D1  D2  …  Dl
A1  A2  …  Am  C1  .. ..  Ck 
B1  .. ..  Bn  D1  D2  …  Dl
 Correctness: clear due to:
 make from all other disjuncts negated body atoms,
 apply generalized modus ponens,
 move all these negated body atoms back as
disjuncts in the head.
9
Resolution: predicate logic
A1  A2  …  Am  B1  …  B  …  Bn
C1  ...  B’  …  Ck  D1  D2  …  Dl
(A1  A2  …  Am  C1  .. ..  Ck)  
(B1  .. ..  Bn  D1  D2  …  Dl) 
where  = mgu(B,B’).
 Correctness:
with a help of the correctness result for the
ground case, applied to all instances of this rule
10
Also in other forms:
 In conjunctive normal form:
A1  A2  …  Am  ~B1  …  ~B  …  ~Bn
C1  ...  B’  …  Ck  ~D1  ~D2  …  ~Dl
(A1  A2  …  Am  C1  .. ..  Ck)  
(~B1  .. ..  ~Bn  ~D1  ~D2  …  ~Dl) 
 with  = mgu(B,B’).
11
Once again Moore’s example
blue(Block1)
red(Block3)
blue(Block2)  red(Block2)
next_to(Block1,Block2)
next_to(Block2,Block1)
next_to(Block2,Block3)
next_to(Block3,Block2)
false  next_to(b1,b2)  blue(b1)  red(b2)
blue(Block2)  red(Block2)
red(Block2)  next_to(Block2,b2)  red(b2)
red(Block3)
red(Block2)  next_to(Block2,Block3)
red(Block2)
next_to(Block2,Block3)
false  next_to(b1,b2)  blue(b1)  red(b2)
false  next_to(b1,Block2)  blue(b1)
false  next_to(Block1,Block2)
blue(Block1)
next_to(Block1,Block2)
false 
12
Ph.D. example
highly_qualified(x)  phd(x)
earn_early(x)  phd(x)
rich(x)  highly_qualified(x)
rich(x)  earn_early(x)
(1)
(2)
(3)
(4)
false  rich(I)
earn_early(x)  phd(x)
highly_qualified(y)  phd(y)
earn_early(x)  highly_qualified(x)
rich(y)  highly_qualified(y)
earn_early(x)  rich(x)
rich(y)  earn_early(y)
rich(x)  rich(x)
rich(x)
factoring
false  rich(I)
false 
13
Factoring: in general
 Both:
A1  A2  …  Am  B1  …  B  …  B’ …  Bn
(A1  A2  …  Am  B1  …  B  … 
…  Bn) 
with:  is mgu(B,B’)
 as:
A1  …  A  …  A’ …  Am  B1  …  Bn
(A1  …  A  … 
…  Am  B1  …  Bn) 
with:  is mgu(A,A’) .
14
Why do we need factoring?
 Without factoring resolution is not complete !
 Example: prove {(p  ~p)  (q  ~q)} inconsistent
 Normalization:
(p  q)  (p  ~q)  (~p  q)  (~p  ~q)
 Clausal form:
pq
pq
pp
qp
false  p  q
qq
pq
qp
You can never get false  !!!!
15
Reason?
 The length of a formula = the number of atoms
(false not included):
Length
N
M
A1  A2  …  Am  B1  …  B  …  Bn
C1  ...  B’  …  Ck  D1  D2  …  Dl
(A1  A2  …  Am  C1  .. ..  Ck)  
(B1  .. ..  Bn  D1  D2  …  Dl) 
N+M-2
 In the previous example all formulas had length 2
You can NEVER get false  (length 0) !
16
The resolution procedure
S:= initial theory (inconsistency to be shown);
Consistent:= false;
Inconsistent:= false;
While not(Consistent) and not(Inconsistent) do
If false   S Then Inconsistent := true
Else
If S contains no pair (F,G) resolvable and not
yet resolved
Then Consistent:= true
Else SELECT a pair (F,G) from S, resolvable
and not yet resolved;
H:= factor( resolvent (F,G) );
S:= S  H
End-while
17
Behavior under Horn
clause resolution :
false  ...
…  ...
false  ...
…  ...
false  ...
…  ...
...
false 
Linear resolution !
18
Behavior under
General resolution :
…  ...
…  ...
…  ...
…  ...
…  ...
…  ...
…  ...
…  ...
false 
General resolution !
19
Linear resolution:
 The most important differences with Horn clauses:
 With Horn clauses the proofs are always LINEAR !
 we start with the “goal”
 we apply a Horn clause to compute a new goal
 etc.
 Clausal resolution is NOT linear
 Also: factoring is sometimes needed
 Linear resolution (a proof is a linear sequence of
resolution steps starting with a goal) is one of the
most important strategies to make the resolution
process efficient.
20
Non-determinism in the
resolution procedure
 SELECT a pair (F,G) : makes it a VERY nondeterministic procedure.
 The control problem for resolution is extremely
difficult.
A proof is no longer 1 (linear) branch in a tree, but a
subgraph of all possible resolutions.
 Is it correct? Is it complete? ?
Is there a complete strategy ???
21
Correctness / Completeness ?
 Completeness: There exists a complete strategy
(standard example: the Herbrand theorem prover).
 Correctness:
If the procedure returns Inconsistent:
 Then false  is added
 Then false  is logically entailed by S
(since the resolution step is correct).
 Thus, in all models of S false  is also true
 Thus, S has no models
22
Correctness/Completeness 2 ?
If the procedure returns Consistent:
 Then ALL POSSIBLE resolution steps were done
without discovering false  .
…  ...
…  ...
…  ...
…  ...
…  ...
…  ...
false
…  …
…  ...
…  ...
…  ...
 Now assume that the set was inconsistent.
 There exists a COMPLETE strategy: that after
some time derives false 
 But it performs (a part of) the same resolution
steps !!
Our strategy also produced false 
23
AR for full predicate logic
Normalization to clausal form
What else is needed for full
predicate logic?
NOTHING!
 Clausal logic is equivalent to full predicate logic:
 every theory T in FOL (first order predicate
logic) can automatically be converted in a clausal
theory T’, such that:
T is inconsistent iff T’ is inconsistent
25
Propositional: via
conjunctive normal form:
 Every formula is equivalent to a formula of the
form:
(A1  ...  An)  (B1  …  Bm)  …  (C1  …  Ck)
where all Ai, Bi, …, Ci are either atomic or ~atomic.
 Idea:
pq
pq
push all ~ as deep as possible
apply distributivity of  and 
pqqp
q  ~p
 Finally:
p1  …  pn  ~q1  … ~qm
p1  …  pn  q1  …  qm
26
Predicate case: main steps
 Prenix normal form
(Q1 x) (Q2 y) …(Qn z) F
 or 
has no quantifiers !
Sometimes requires new variable names.
Ex.: x p(x)  x q(x)
x z p(x)  q(z)
Note: x cloudy(x)  x sunny(x) is not equivalent to
x cloudy(x)  sunny(x)
 Conjunctive normal form:
(Q1 x) (Q2 y) …(Qn z) ( ..  .. )  ( ..  .. )  ..  ( ..  .. )
These 2 steps are interleaved.
27
Predicate case: continued
 Skolem normal form: transform to:
( x) ( y) …( z) ( ..  .. )  ( ..  .. )  ..  ( ..  .. )
 x rich(x) is replaced by rich(Sk) , with Sk being a
new constant (‘skolem constant’) that does not
appear in the alphabet.
 More complex: if  appears nested inside :
 ‘Everyone has a heart’
x person(x)  y heart(y)  has(x,y)
 Not correct:
x person(x)  heart(H)  has(x,H)
 Correct: x person(x)  heart(H(x))  has(x,H(x))
Skolem functions: as many arguments as enclosing -variables
28
Predicate case: continued
 Disjunctions:
x y z (p(x)  ~q(y)  ~r(y))
 (r(A)  q(z))
 ~s(x,y)
S = {x y (p(x)  ~q(y)  ~r(y)) ,
z (r(A)  q(z)) ,
x y ~s(x,y) }
 Clausal form:
S = {p(x)  q(y)  r(y) ,
r(A)  q(z)) ,
false  s(x,y) }
29
Explicit Procedure:
1. Eliminate  en  .
2. Move the negations inside:
~(~p)  p, ~(p  q)  ~p  ~q, (analogously for )
~x  x ~ , ~x  x ~
3. Standardize variable names (make them different).
4. Move quantifiers to front.
PRENEX NORMAL FORM
5. Eliminate  .
6. Disjunctions inside.
INTRODUCE SKOLEMS
7. Drop .
8. Drop .
9. ~atoms to the other side.
DISJUNC. SET
CONJUNCTIVE FORM
CLAUSAL FORM
30
Marcus example:
 Facts 1. , 2. , 4. and 8. were already o.k.:
 ex.: ruler(Caesar)
 3. x Pompeian(x)  Roman(x) : o.k. !
 6. x y loyal_to(x,y)
x loyal_to(x,f(x))
loyal_to(x,f(x))
 7. xy man(x)  ruler(y)  try_assassinate(x,y) 
~loyal_to(x,y)
xy ~(man(x)  ruler(y)  try_assassinate(x,y))  ~loyal_to(x,y)
xy ~man(x)  ~ruler(y)  ~try_assassinate(x,y)  ~loyal_to(x,y)
false  man(x)  ruler(y)  try_assassinate(x,y)  loyal_to(x,y)
31
Axioms in Normal form:
1. man(Marcus)
2. Pompeian(Marcus)
3. Roman(x)  Pompeian(x)
4. ruler(Caesar)
5. loyal_to(x,Caesar)  hates(x,Caesar)  Roman(x)
6. loyal_to(x,f(x))
7. false  man(x)  ruler(y)  try_assassinate(x,y) 
loyal_to(x,y)
8. try_assassinate(Marcus,Caesar)
To show:
Negation:
Normal Form:
hates(Marcus,Caesar)
~hates(Marcus,Caesar)
false  hates(Marcus,Caesar)
32
Resolution proof (1):
false  hates(Marcus,Caesar)
{x/Marcus}
5.
loyal_to(x,Caesar)  hates(x,Caesar)  Roman(x)
loyal_to(Marcus,Caesar)  Roman(Marcus)
{x/Marcus}
3.
Roman(x)  Pompeian(x)
loyal_to(Marcus,Caesar)  Pompeian(Marcus)
{}
2.
Pompeian(Marcus)
loyal_to(Marcus,Caesar)
33
Resolution proof (2)
loyal_to(Marcus,Caesar)
7.
false  man(x)  ruler(y)  try_assassinate(x,y)  loyal_to(x,y)
{x/Marcus,y/Caesar}
false  man(Marcus)  ruler(Caesar)  try_assassinate(Marcus,Caesar)
{}
1. man(Marcus)
false  ruler(Caesar)  try_assassinate(Marcus,Caesar)
4.
ruler(Caesar)
{}
8.
false  try_assassinate(Marcus,Caesar)
try_assassinate(Marcus,Caesar)
{}
false 
34
Example from Group Theory:
 Let  be a group operation.
 Prefix notation: p(x,y,z)  x  y = z
 Definition of a monoid, with left-neutral and left
inverse element:
  is defined for all elements of the set:
xyz p(x,y,z)
  is associative:
(1)
(x  y)  z = x  (y  z)
u
v
xyzuvw
(p(x,y,u)  p(y,z,v))  (p(u,z,w)  p(x,v,w))
(2)
35
Example from
Group Theory (2):
  has a left neutral and a left inverse element:
x (y p(x,y,y)  yz p(z,y,x)
(3)
 Theorem: there exists also a right inverse !
x (y p(x,y,y)  yz p(y,z,x)
(4)
 To be proved automatically by resolution.
36
Normalization:
(1) xyz p(x,y,z)
 Steps: 1,2,3,4: o.k.
 Step 5: skolemization:
xy p(x,y,m(x,y))
 Steps: 6,7: o.k.
 Step 8: clausal form:
p(x,y,m(x,y))
37
Normalization (continued):
(2) xyzuvw
(p(x,y,u)  p(y,z,v)) 
(p(u,z,w)  p(x,v,w))
 Step 1: eliminate  and  :
xyzuvw (p(x,y,u)  p(y,z,v)) 
((p(u,z,w)  p(x,v,w))  (p(x,v,w)  p(u,z,w)))
xyzuvw (p(x,y,u)  p(y,z,v)) 
((~p(u,z,w)  p(x,v,w))  (~p(x,v,w)  p(u,z,w)))
xyzuvw ~(p(x,y,u)  p(y,z,v)) 
((~p(u,z,w)  p(x,v,w))  (~p(x,v,w)  p(u,z,w)))
38
Normalization (continued):
xyzuvw ~(p(x,y,u)  p(y,z,v)) 
((~p(u,z,w)  p(x,v,w))  (~p(x,v,w)  p(u,z,w)))
 Step 2: move negation inside:
A
xyzuvw
(~p(x,y,u)  ~p(y,z,v)) 
((~p(u,z,w)  p(x,v,w))  (~p(x,v,w)  p(u,z,w)))
(B  C)
 Steps: 3,4,5 o.k.
 Step 6: move disjunctions inside:
A  (B  C) = (A  B)  (A  C)
A B
xyzuvw
((~p(x,y,u)  ~p(y,z,v))  (~p(u,z,w)  p(x,v,w))) 
((~p(x,y,u)  ~p(y,z,v))  (~p(x,v,w)  p(u,z,w)))
A C
39
Normalization (continued):
xyzuvw
((~p(x,y,u)  ~p(y,z,v))  (~p(u,z,w)  p(x,v,w))) 
((~p(x,y,u)  ~p(y,z,v))  (~p(x,v,w)  p(u,z,w)))
+ remove redundant parentheses: ( )
xyzuvw
(~p(x,y,u)  ~p(y,z,v)  ~p(u,z,w)  p(x,v,w)) 
(~p(x,y,u)  ~p(y,z,v)  ~p(x,v,w)  p(u,z,w))
 Steps 7,8: eliminate  en  :
~p(x,y,u)  ~p(y,z,v)  ~p(u,z,w)  p(x,v,w)
~p(x,y,u)  ~p(y,z,v)  ~p(x,v,w)  p(u,z,w)
40