AR4 Clausal Eng

AR: clausal logic: 

AR: clausal logic The step to Resolution

Clausal form: 

Clausal form 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.

Example: Moore’s problem: 

Example: Moore’s problem Given 3 blocks: Prove that there is a blue block next to a red block!

Moore’s problem (2):: 

Moore’s problem (2): PROBLEM: Modus ponens is not suitable for blue(block2)  red(block2)

Introducing negation in bodies is equivalent:: 

Introducing negation in bodies is equivalent: Example:

Disjunction versus negation in general:: 

Disjunction versus negation in general: x1 … xk A1  A2 …  Am  B1  B2 …  Bn

The resolution principle: 

The resolution principle Propositional case: 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.

Resolution: predicate logic: 

Resolution: predicate logic where  = mgu(B,B’). Correctness: with a help of the correctness result for the ground case, applied to all instances of this rule

Also in other forms:: 

Also in other forms: In conjunctive normal form: with  = mgu(B,B’). A1  A2  …  Am  ~B1  …  ~B  …  ~Bn C1  ...  B’  …  Ck  ~D1  ~D2  …  ~Dl (A1  A2  …  Am  C1  .. ..  Ck)   (~B1  .. ..  ~Bn  ~D1  ~D2  …  ~Dl) 

Once again Moore’s example: 

Once again Moore’s example false  next_to(b1,b2)  blue(b1)  red(b2)

Ph.D. example: 

Ph.D. example

Factoring: in general: 

Factoring: in general

Why do we need factoring?: 

Why do we need factoring? (p  q)  (p  ~q)  (~p  q)  (~p  ~q) Without factoring resolution is not complete ! Example: prove {(p  ~p)  (q  ~q)} inconsistent Normalization: Clausal form: You can never get false  !!!!

Reason?: 

Reason? The length of a formula = the number of atoms (false not included): N M N + M - 2 In the previous example all formulas had length 2

The resolution procedure: 

The resolution procedure S:= initial theory (inconsistency to be shown); Consistent:= false; Inconsistent:= false; If false   S Then Inconsistent := true If S contains no pair (F,G) resolvable and not yet resolved Then Consistent:= true H:= factor( resolvent (F,G) ); S:= S  H End-while

Behavior under Horn clause resolution :: 

Behavior under Horn clause resolution : false  Linear resolution !

Behavior under General resolution :: 

Behavior under General resolution : General resolution !

Linear resolution:: 

Linear resolution: The most important differences with Horn clauses: 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.

Non-determinism in the resolution procedure: 

Non-determinism in the resolution procedure SELECT a pair (F,G) : makes it a VERY non-deterministic 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? ?

Correctness / Completeness ?: 

Correctness / Completeness ? Correctness: 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

Correctness/Completeness 2 ?: 

Correctness/Completeness 2 ? If the procedure returns Consistent: Then ALL POSSIBLE resolution steps were done without discovering 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 !!

AR for full predicate logic: 

AR for full predicate logic Normalization to clausal form

What else is needed for full predicate logic?: 

What else is needed for full predicate logic? 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

Propositional: via conjunctive normal form:: 

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.

Predicate case: main steps: 

Predicate case: main steps These 2 steps are interleaved.

Predicate case: continued: 

Predicate case: continued 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 :

Predicate case: continued: 

Predicate case: continued Clausal form: x y z (p(x)  ~q(y)  ~r(y))  (r(A)  q(z))  ~s(x,y) Disjunctions:

Explicit Procedure:: 

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). 8. Drop .

Marcus example:: 

Marcus example: 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) 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) 7. xy man(x)  ruler(y)  try_assassinate(x,y)  ~loyal_to(x,y)

Axioms in Normal form:: 

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: hates(Marcus,Caesar) Negation: ~hates(Marcus,Caesar) Normal Form: false  hates(Marcus,Caesar)

Resolution proof (1):: 

Resolution proof (1): false  hates(Marcus,Caesar)

Resolution proof (2): 

Resolution proof (2) loyal_to(Marcus,Caesar)

Example from Group Theory: : 

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: (x  y)  z = x  (y  z) xyzuvw (p(x,y,u)  p(y,z,v))  (p(u,z,w)  p(x,v,w)) (1) (2)

Example from Group Theory (2):: 

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) Theorem: there exists also a right inverse ! (3) x (y p(x,y,y)  yz p(y,z,x) (4) To be proved automatically by resolution.

Normalization:: 

Normalization: (1) xyz p(x,y,z) Steps: 1,2,3,4: o.k. Step 5: skolemization: Steps: 6,7: o.k. Step 8: clausal form: p(x,y,m(x,y))

Normalization (continued):: 

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)))

Normalization (continued):: 

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))) 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: Steps: 3,4,5 o.k. Step 6: move disjunctions inside: 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  (B  C) = (A  B)  (A  C)

Normalization (continued):: 

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))) 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  :