Inference in FOPL PDF

Inference in FOPL Artificial intelligence Kristóf Karacs PPKE-ITK Goal-based Agents Agent Sensors State Percepts What the w...

Inference in FOPL Artificial intelligence Kristóf Karacs PPKE-ITK Goal-based Agents Agent Sensors State Percepts What the world How the world is like now? evolves? Environment What my actions do? What it will be if I do action A? What action Goals should I do now? Actions Actuators Search & Planning 1 Logical inference schemes n Deduction: formal logical reasoning ¨ Premises: 1. All men are mortal. 2. Aristotle is a man. ¨ Conclusion: Aristotle is mortal. n Induction: generalization ¨ Premise: The sun has risen in the east every morning up until now. ¨ Conclusion: The sun will also rise in the east tomorrow. n Abduction: choosing an explanation ¨ Premise: 1. Flu causes fever. 2. Peter has fever. ¨ Conclusion: Peter has flu. The case of the silk gloves “It was elementary my dear Watson. The killer always left a silk glove at the scene of the murder. That was his calling card. Our investigations showed that only three people have purchased such gloves in the past year. Of these, Professor Doolally and Reverend Fisheye have iron- clad alibis, so the murderer must have been Sergeant Heavyset. When he tried to murder us with that umbrella, we knew we had our man.” 2 Not so elementary… “The killer always left a silk glove at the scene of the murder.” (induction) “That was his calling card.” (abduction) “…only three people have purchased such gloves in the past year.” (model generation) “Professor Doolally and Reverend Fisheye have iron-clad alibis.” (constraint based reasoning) “…so the murderer must have been Sergeant Heavyset.” (deduction) First Order Predicate Logic (FOPL) n Most used and analyzed logic n Completeness: Gödel, Herbrand, 1930 ¨ If a FOPL statement is valid then it is provable ¨ If KB ⊨ a then KB ⊢ a ¨ FOPL rules are enough to prove all logically valid formulae n Validity is semi-decidable n Resolution: Robinson, 1963 3 Chains of inference n Remember the problem we are trying to solve ¨ Search for a path from axioms ai, to theorem T n Three approaches ¨ Forward chaining ¨ Backward chaining ¨ Proof by contradiction n Specification of a search problem: ¨ Representation of states (first order predicate logic sentences) ¨ Initial state (changes with the approach) ¨ Operators (rules of inference, usually implication rules) ¨ Goal state (changes with the approach) Forward Chaining n Start with initial axioms (atomic sentences) and deduce new facts by applying modus ponens n Repeat until possible or query is answered n Problems ¨ Generates many irrelevant facts ¨ Every rule has to be rechecked whenever a new fact is added to KB a1 a2 a3 T 4 Forward Chaining n A first-order definite clause is a disjunction of literals of which exactly one is positive ¨ Example n white(X) Ù potable(X) ® milk(X) is logically equivalent to ¬white(X) Ú ¬ potable(X) Ú milk(X) ¨ Modus ponens can be easily applied to first-order definite clauses ¨ All variables are implicitly universally quantified n Sound, complete Backward Chaining n Work backwards from the goal, chaining rules to find facts that support the conclusion n For each node the inference rule has to be inverted ¨ Which operator could have been applied to which state to produce this state (sentence) n No problem when using equivalences ¨ Can also use a bidirectional search (from both ends) n Difficult when using implications ¨ Many possible ways to invert operators n Works in a DFS like manner ® incomplete n Still popular and effective 5 Proof By Contradiction n “Reductio ad absurdum” n Most often used method n Idea: by showing that the assumption contradicts a set of axioms we can prove that the assumption is false n KB’ = Set of axioms (KB) + negated theorem (¬Th) n If the F statement can be deduced from KB’ then ¬Th is false, and thus Th must be true n Advantage: heuristic function can be defined based on the distance from the ‘False’ statement Completeness of resolution 6 First order implication rules n Propositional implications and equivalences n First order implication rules ¨ Quantifiers ¨ Variables ¨ Substitution Universal elimination n In a sentence j any universally quantified variable v can be replaced by any ground term g "v j subst({v/g}, j) n Note: the variable has to be removed from quantification n Example ¨ "x friend(Sue, x) becomes friend(Sue, Ann) 7 Existential introduction n In a sentence j any ground term g can be substituted by a variable v if it does not appear in j j $v subst({g/v}, j) n Example ¨ friend(Sue, Ann) becomes $x friend(Sue, x) n Exercise ¨ Find a sentence where v is in j such that this implication rule is not sound Universal introduction n In a sentence j any constant k can be substituted by a variable v if k is not mentioned in any of the premises or undischarged assumptions and v does not appear in j j "v subst({k/v}, j) n Example ¨ friend(Sue, Doe) becomes "x friend(Sue, x) 8 Existential elimination n In a sentence j any existentially quantified variable v can be replaced by any constant k, if k appears neither in j nor anywhere else in the derivation $v j subst({v/k}, j) n k is called a Skolem constant n Existential elimination is a special case of skolemization (see later) Propositionalization n Universal and existential elimination allow for inferring non-quantified sentences from quantified ones n Reduces first-order inference to propositional inference n Problem ¨ Function symbols allow infinitely many ground terms: father(father (father (...))) ¨ Can be overcome by Herbrand’s theorem n “If a set S of clauses is unsatisfiable, then there exists a finite subset of HS(S) that is also unsatisfiable.” n Entailment in FOPL is semi-decidable (Church) ¨ Any entailed sentence can be proven ¨ Non-entailed sentences cannot be disproven (Halting problem) 9 Inference with variables n Premise n "x (knows(Bob, x) ® loves(Bob, x)) n From “knows(Bob, Alice)” n using modus ponens gives: “loves(Bob, Alice)” n From “knows(Bryan, Alice)” n modus ponens cannot be used n How to check applicability when variables are present? Unifying predicates n Expressions x1 and x2 are unifiable iff there exists a substitution Q such that subst(Q, x1) = subst(Q, x2), where subst(Q, x) applies Q to x n Unification by substitution ({X/Alice}) ¨ knows(Bob, X) and knows(Bob, Alice) n Possibilities ¨ variable-variable ¨ variable-constant ¨ variable-function 10 The unification algorithm n A recursive algorithm ¨ Passes around a set of substitutions, called mu ¨ Makes sure that new substitutions are consistent with old ones n unify(x,y) = unify_internal(x,y,{}) ¨ x and y can be variables, constants, lists, or compounds n unify_internal(x,y,mu) ¨ x and y are sentences, mu is a set of substitutions ¨ finds substitutions making x look exactly like y n unify_variable(var,x,mu) ¨ var is a variable ¨ finds a single substitution (which may be in mu already) unify_internal unify_internal(x,y,mu) 1.if (mu==failure) then return failure 2.if (x==y) then return mu 3.if (isa_variable(x)) then return unify_variable(x,y,mu) 4.if (isa_variable(y)) then return unify_variable(y,x,mu) 5.if (isa_compound(x) & isa_compound(y)) then return unify_internal(args(x),args(y), unify_internal(op(x),op(y),mu)) 6.if (isa_list(x) & isa_list(y)) then return unify_internal(tail(x),tail(y), unify_internal(head(x),head(y),mu)) 7.return failure 11 unify_variable unify_variable(var,x,mu) 1. if (a substitution var/val is in mu) then return unify_internal(val,x,mu) 2. if (a substitution x/val is in mu) then return unify_internal(var,val,mu) 3. if (var occurs anywhere in x) return failure 4. add var/x to mu and return Notes on the unification algorithm n unify_internal will not match a constant to a constant, unless they are equal (case 2) n Case 5 in unify_internal checks that two compound operators are the same (e.g., same predicate name) n Case 6 in unify_internal causes the algorithm to recurse covering the whole list n Cases 1 and 2 in unify_variable check that neither inputs have already been substituted 12 The occurs check n When substituting variable x with an expression f(x,y) ¨ x will be replaced by f(x,y) ¨ But f(x,y) still contains an instance of x, which has to be replaced again ¨ We get f(f(x,y),y), and then f(f(f(x,y),y),y), etc. ¨ Infinite recursion the algorithm will not stop (halt) n Case 3 in unify_variable checks this to avoid this situation n Problem: Occurs check slows down the algorithm ¨ Its complexity is O(n2), where n is the size of expressions being unified Unification exercises n nice(Alice) – nice(Mary) n sees(x,Alice) – sees(y,Alice) n sees(x,Alice) – sees(Mary,y) n x – child(Alice,x) n friends(x,y,Alice) Ù father(sonof(Bob),Bob) – father(z,Bob) Ù friends(Mary,z,u) n R(F(y),x) – R(x,F(A)) n R(F(y),y,x) – R(x,F(A),F(v)) n F(G(w),H(w,J(x,u))) – F(G(v),H(u,v)) n F(x,F(u,x)) – F(F(y,A),F(z,F(B,z))) 13 Full resolution rule n Resolution rules remove predicates in predicate logic ¨ This is known as resolving the two sentences n Unit resolution rule (AÚB), ¬B A n Full resolution rule (using CNF) (AÚB), (¬BÚC) AÚC n With implication (¬A®B), (B®C) ¬A®C Generalized resolution rule n Given two CNF sentences p1 Ú p2 Ú … Ú pm and q1 Ú q2 Ú … Ú qn n If pj and ¬qk can be unified, i.e. unify(pj, ¬qk) = Q, then p1 Ú … Ú pj Ú … pm, q1 Ú … Ú qk Ú … Ú qn subst(Q , (p1 Ú … pj-1 Ú pj+1 Ú … Ú pm Ú q1 Ú … Ú qk-1 Ú qk+1 Ú … qn)) 14 Resolution with variables n P(x) Ú Q(x, y) n ¬P(A) Ú R(B, z) n subst({x/A}, Q(x, y) Ú R(B, z)) n Q(A, y) Ú R(B, z) Local variable scope n P(x) Ú Q(x, y) n ¬P(A) Ú R(B, x) 15 Local variable scope n P(x1) Ú Q(x1, y) n ¬P(A) Ú R(B, x2) n subst({x1/A}, Q(x1, y) Ú R(B, x2)) n Q(A, y) Ú R(B, x2) CNF in FOPL n Sentences need to be in conjunctive normal form (CNF) ¨ Literalscan contain variables, assumed to be universally quantified n Example ¨ white(X)Ù potable(X) ® milk(X) becomes ¬white(X) Ú ¬ potable(X) Ú milk(X) 16 Conversion to clausal form n 1. Eliminate ® and « n 2. Drive in ¬ to atomic level n 3. Rename variables apart n 4. Skolemize n 5. Drop universal quantifiers n 6. Convert to CNF n 7. Rename variables in each clause Skolemization n Substitute a new constant for each existentially quantified variable ¨ $xP(x) P(CS) n Substitute a new function of all universally quantified variables in enclosing scopes for each existentially quantified variable ¨ "x $y P(x, y) "x P(x, fS(x)) 17 “A cat called Tuna” (from textbook) n Jack owns a dog n Every dog owner is an animal lover n No animal lover kills an animal. n Either Jack or Curiosity killed the cat, who is named Tuna. n Did Curiosity kill the cat? A. $x (Dog(x) Ù Owns(Jack,x)) B. "x ( (($y) Dog(y) Ù Owns(x, y)) ® AnimalLover(x) ) C. "x (AnimalLover(x) ® (("y) Animal(y) ® ¬Kills(x,y))) D. Kills(Jack,Tuna) Ú Kills(Curiosity,Tuna) E. Cat(Tuna) F. "x (Cat(x) ® Animal(x) ) G. Kills(Curiosity, Tuna) Conversion to clausal form n 1. Eliminate ® and « n 2. Drive in ¬ to atomic level n 3. Rename variables apart n 4. Skolemize n 5. Drop universal quantifiers n 6. Convert to CNF n 7. Rename variables in each clause 18 Using resolution n Choose two clauses ¨ Choose a positive literal P from one with its negative N in the second ¨ Find MGU q of P and ¬N ¨ If successful, then join the two clauses in a single disjunction n With P and N missing n Apply q to the new clause Resolution proof as search n Keep on resolving clause pairs ¨ Eventually result in zero-length clause ¨ This indicates that some literal K was true at the same time as the literal ¬K n Only way to reduce sentence to be empty ¨ Hence there was an inconsistency ¨ Which proves the theorem 19 Sentence A & B n (A) $x. Dog(x) Ù Owns(Jack,x) n Dog(D) Ù Owns(Jack,D) n (B) "x. ( $y. Dog(y) Ù Owns(x,y)) ® AnimalLover(x) n "x. ( ¬$y. Dog(y) Ù Owns(x,y)) Ú AnimalLover(x) n "x. "y. ¬(Dog(y) Ù Owns(x,y)) Ú AnimalLover(x) n "x. "y. ¬Dog(y) Ú ¬Owns(x,y) Ú AnimalLover(x) n ¬Dog(y) Ú ¬Owns(x,y)) Ú AnimalLover(x) Sentence C & D n (C) "x. AnimalLover(x) ® ( "y. Animal(y) ® ¬Kills(x,y)) n "x. ¬AnimalLover(x) Ú ( "y. Animal(y) ® ¬Kills(x,y)) n "x. ¬AnimalLover(x) Ú ( "y. ¬Animal(y) Ú ¬Kills(x,y)) n ¬AnimalLover(x) Ú ¬Animal(y) Ú ¬Kills(x,y) n (D) Kills(Jack,Tuna) Ú Kills(Curiosity,Tuna) 20 Sentence E, F and neg. Th. n (E) Cat(Tuna) n (F) "x. Cat(x) ® Animal(x) n ¬Cat(x) Ú Animal(x) n (Th) ¬Kills(Curiosity,Tuna) Solution n (D), (Th) Kills(Jack,Tuna) (G) n (E), (F), {x/T} Animal(Tuna) (H) n (C), (G), {x/J, y/T} ¬AnimalLover(Jack) Ú ¬Animal(Tuna) (I) n (H) , (I) ¬AnimalLover(Jack) (J) n (B), (J), {x/J} ¬Dog(y) Ú ¬Owns(Jack,y) (K) n (A2) ¬Dog(D) (L) n (A1), (L) False 21 CNF (Implicative form) n Jack owns a dog n Every dog owner is an animal lover n No animal lover kills an animal. n Either Jack or Curiosity killed the cat, who is named Tuna. n Did Curiosity kill the cat? A1. Dog(D) A2. Owns(Jack,D) B. Dog(y) Ù Owns(x,y) ® AnimalLover(x) C. AnimalLover(x) Ù Animal(y) ® ØKills(x,y) D. Kills(Jack,Tuna) Ú Kills(Curiosity,Tuna) E. Cat(Tuna) F. ØCat(x) Ú Animal(x) Graph of proof 22 Equality n Unification of different constants ¨ Today(Thu), Today(Thursday) n Expanding the KB is not sufficient ¨ Thu = Thursday n Extra axioms are needed ¨ Equality is symmetric, reflexive and transitive n Equality statements for each predicate: n "x,y x = y ® (P(x) « P(y)) etc. Demodulation rule n Takes two input sentences, one expressing an equality (a = b) n Finds a unification for a with a term in another clause (Q = unify(a, g)) n Applies Q to b (not a) n Replaces occurrence of g with Subst(Q, b) a = b, (…, g,…) (…,Subst(Q, b),…) 23 Demodulation drawbacks n Cannot bind variables in expression ¨ father(Adam) = Bob a = b, (…, g,…) n a: father(Adam) , b: Bob ¨ older(father(x), x) Q = unify(a, g) n g: father(x), Q = {x/Adam}, (…, Subst(Q, b), …) Subst(Q, b) = Bob ¨ older(Bob, Adam) : not derived, only older(Bob, x) n Equation must be a unit clause ¨ (x = Adam Ù y = Bob) ® father(x) = y n a cannot be father(x), since the equation is inside an implication ¨ older(father(x), x) ¨ (x = Adam Ù y = Bob) ® older(Bob, Adam) Paramodulation n F(x) = B n a Ú (s = t) n Q(y) Ú W(y,F(y)) n b Ú g [r] Q = unify(s,r) n Q(y) Ú W(y,B) n Subst(Q,(a Ú b Ú g [r])) n G(x) Ú F(x) = B n s = F(x); t=B n Q(y) Ú W(y,F(y)) n g[⋅] =W (y,⋅); r = F(y) n G(y) Ú Q(y) Ú W(y,B) n Q = {x/y} 24 Horn clauses n Have the form: P1 Ù P2 Ù … Ù Pn ® Q n Special cases ¨ P1 Ù P2 Ù … Ù Pn ® False ¨ True ® Q n Enables polynomial time inference n Prolog (SLD resolution) ¨ S: Selection function ¨ L: Linear sequence of clauses ¨ D: Definite clauses ¨ Ordered resolution Sample Prolog program fun(X) :- car(vw_beatle). red(X), car(ford_escort). bike(harley_davidson). car(X). red(vw_beatle). red(ford_escort). fun(X) :- blue(harley_davidson). blue(X), bike(X). ?- fun(harley_davidson). true 25 Resolution proving as search n Search space: Sentences in FOPL n Initial state: {KB, ¬Th.} n Operator: generalized resolution inference rule n Goal Check: Empty clause found n Solution: two possibilities ¨ Path from axioms to false clause (if we want proof) ¨ Just the fact that we have reached the false clause (no proof required) Elimination strategies n Identical clause elimination ¨ Clauses occurring twice can be removed and all proofs will still be possible n Pure literal elimination ¨A literal with no negated occurrence makes its clause superfluous n Tautology elimination ¨ No effect on satisfiability n Subsumption elimination ¨ Remove clauses that are more specific than others in the KB 26 Restriction strategies n Unit resolution ¨ One resolvent is always a unit clause (single literal) n Input resolution ¨ One resolved clause is always taken from initial KB ¨ Complete, if the KB contains Horn clauses n Linear resolution ¨ One resolved clause is always taken from either the initial KB or from the ancestor of the other resolvent; Complete n Set of Support ¨ One resolvent is always taken from a subset of initial KB or from its descendant ¨ Complete, if the clauses outside the SoS are satisfiable n Ordered resolution ¨ Clauses are treated as ordered sets, resolution is allowed only on the first literal Applications of resolution n Automated Theorem Proving (ATP) n Proof verification n Proof compression n Automated Conjecture Making n Interactive proving n Proof planning 27 A famous example for ATP n Axiomatization of Boolean algebra n Standard axioms ¨ "a, b Î B a+b = b+a ¨ "a, b, c Î B (a+b)+c = a+(b+c) ¨ $0 Î B (unit element for +) 0 + a =a ¨ "a Î B ¬¬a = a ¨ "a Î B ¬(a + ¬a) = 0 ¨ "a, b, c Î B a + ¬(¬b + ¬c) = ¬(¬(a+b) + ¬(a+c)) Robbins Problem n Huntigton’s proposal to axiomatize Boolean algebras (1933) ¨ Commutativity + associativity ¨ "a, b Î B. a = ¬(¬a + b) + ¬(¬a + ¬b) n Herbert Robbins ¨ Commutativity + associativity ¨ "a, b Î B. a = ¬(¬(a + b) + ¬(a + ¬b)) ¨ Got coined “Robbins algebra” 28 Solving the Robbins Problem n William McCune and Larry Wos ¨ Argonne National Laboratories ¨ EQP & Otter (first order provers) ¨ EQP solved this in 8 days, completed on Oct. 10,1996 ¨ One step from the proof: ¬(¬(¬(¬(¬(x) + x) + ¬(¬(x) + x) + x + x + x + x) + ¬(¬(¬(x) + x) + x + x + x) + x) + x) = ¬(¬(¬(x) + x) + ¬(¬(x) + x) + x + x + x + x) ¨ Otter proved that the proof is OK (its successor is called Prover9) ----- EQP 0.9, June 1996 ----- The job began on eyas09.mcs.anl.gov, Wed Oct 2 12:25:37 1996 UNIT CONFLICT from 17666 and 2 at 678232.20 seconds. ---------------- PROOF ---------------- 2 (wt=7) [] -(n(x + y) = n(x)). 3 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y. 5 (wt=18) [para(3,3)] n(n(n(x + y) + n(x) + y) + y) = n(x + y). 6 (wt=19) [para(3,3)] n(n(n(n(x) + y) + x + y) + y) = n(n(x) + y). 24 (wt=21) [para(6,3)] n(n(n(n(x) + y) + x + y + y) + n(n(x) + y)) = y. 47 (wt=29) [para(24,3)] n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + z) + n(y + z)) = z. 48 (wt=27) [para(24,3)] n(n(n(n(x) + y) + n(n(x) + y) + x + y + y) + y) = n(n(x) + y). 146 (wt=29) [para(48,3)] n(n(n(n(x) + y) + n(n(x) + y) + x + y + y + y) + n(n(x) + y)) = y. 250 (wt=34) [para(47,3)] n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + n(y + z) + z) + z) = n(y + z). 996 (wt=42) [para(250,3)] n(n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + n(y + z) + z) + z + u) + n(n(y + z) + u)) = u. 16379 (wt=21) [para(5,996),demod()] n(n(n(n(x) + x) + x + x + x) + x) = n(n(x) + x). 16387 (wt=29) [para(16379,3)] n(n(n(n(n(x) + x) + x + x + x) + x + y) + n(n(n(x) + x) + y)) = y. 16388 (wt=23) [para(16379,3)] n(n(n(n(x) + x) + x + x + x + x) + n(n(x) + x)) = x. 16393 (wt=29) [para(16388,3)] n(n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) + x) = n(n(x) + x). 16426 (wt=37) [para(16393,3)] n(n(n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) + x + y) + n(n(n(x) + x) + y)) = y. 17547 (wt=60) [para(146,16387)] n(n(n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) + n(n(n(x) + x) + x + x + x) + x) + x) = n(n(n(x) + x) + n(n(x) + x) + x + x + x + x). 17666 (wt=33) [para(24,16426),demod()] n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) = n(n(n(x) + x) + x + x + x). ------------ end of proof ------------- 29 A problem by Lewis Carroll n The only animals in this house are cats n Every animal that loves to gaze at the moon is suitable for a pet n When I detest an animal, I avoid it n No animals are carnivorous unless they prowl at night n No cat fails to kill a mice n No animals ever like me, except those that are in this house n Kangaroos are not suitable for pets n None but carnivorous animals kill mice n I detest animals that do not like me n Animals that prowl at night always love to gaze at the moon n Therefore, I always avoid a kangaroo Summary n FOPL semantics n Chains of inference n Propositionalization n Resolution ¨ Unificationalgorithm ¨ Generalized resolution ¨ Equality ¨ Resolution strategies n Automatic theorem proving 30