CS244 - Lectures 5-6, Sept 28-Oct 5 - Resolution The Lecture Outline is followed by the detailed Lecture Notes. LECTURE OUTLINE ** = important material not in the textbook Ch 3: Representation: Reification **Ontologies **Time Ch 4: Resolution: Kinds of proofs 4.1 Conversion to CNF Resolution derivations A non-deterministic entailment procedure Examples propositional resolution proofs **Size-preserving converson to CNF Proof of correctness of propositional resolution **Proof of completeness of propositional resolution 4.2 Conversion of universally-quantified formulas First-order resolution 4.2.3 Skolemization **Relation of a formula to its Skolemization **Most general unifier algorithm Examples of FOL proofs Answer extraction 4.2.4 Handling equality **Paramodulation 4.3 The Herbrand Theorem **Proof of Herbrand theorem Semi-decidability of FOL **Proof that FOL is not decidable *********************************************************************************** *********************************************************************************** *********************************************************************************** LECTURE NOTES ** = important material not in the textbook Ch 3: Representation: Reification What is point of example: Purchase(sam,bike,200) vs Purchase(p99) & agent(p99)=sam & object(p99)=bike & price(p99)=200 Suppose you don't want to use any function symbols or equality? Purchase(p99) & agent(p99,sam) & ... What does this say about the expressive power of FOL if it is restricted to (at most) 2 place predicates? (Unchanged) Compare to relational database versus XML **Ontologies ontology = fancy word for a classification system Example animal mammal reptile human cat sam bill puff How should this be represented in FOL? Note difference between classes (predicate) and individuals (terms) How to distinguish exhaustive versus non-exhaustive ways of specializing a concept? Inheritance of properties animals have hair therefore, sam has hair No special mechanism needed! Ontologies aren't only about objects, they can be about abstract things like events. Exchange Purchase Gifting Trade OnlinePurchase BrickAndMotarPurchase What are the arguments to these predicates? Purchase(oldowner, newowner, object, price) => Exchange(oldowner, newowner, object) Exchange(oldowner, newowner, object) => E price . Purchase(oldowner, newowner, object, price) v E occasion . Gifting(oldowner, newowner, object, occasion) v E object2 . Gifting(oldowner, newowner, object, object2) Reified approach: Purchase(e) => Exchange(e) Exchange(e) => Purchase(e) v Gifting(e) v Trade(e) **Time How to represent time? Discrete time: add extra argument to predicates: On(box1,box2,time) Linear time: On(box1,box2,time) & Pickup(box2,time) => ~On(box1,box2,next(time)) or, allowing integer arithmetic: On(box1,box2,time) & Pickup(box2,time) => ~On(box1,box2,time+1) Branching time: On(box1,box2,time) => ~On(box1,box2, do(pickup(box1),time) ) Here, actions are FUNCTIONS rather than predicates! A different possible future: On(box1,box2,time) => On(box1,box2, do(paint(box1),time) ) Time intervals: On(box1, box2, starttime, endtime) Reified events: Exchange(e) & time(e)=3 A e . Exchange(e) => Owns(newowner(e), object(e), next(time(e))) **************************************************************************** Ch 4: Resolution: Kinds of proofs: Is a sentence (query) entailed by a knowledge base? Is a sentence valid? Is a set of sentences unsatisfiable? Does a set of sentence entail a false statement? KB |= S |= (KB) => S KB U {~S} is not satisfiable KB U {~S} |= ~TRUE 4.1 Conversion to CNF, propositional case 1. Eliminate => and <=> 2. Move in ~ LITERAL: a propositional atom or its negation 3. Distribute & over V 4. Eliminate repeated literals in a clause 5. Eliminate clauses containing a literal and its negation 6. Erase & and V signs ((Rich v Talented) & ~Addict) => (Famous & Happy) Meaning of an empty CNF {} : true Meaning of an empty clause {{}}: false Resolution derivations class on 9/30/2010 starts here ===> Resolution rule: {P} U C1 + {~P} U C2 ---------------- C1 U C2 Proof that resolution rule is sound using interpretations: Suppose I is an interpretation where I|={P} U C1 I|={~P} U C2 Consider cases: case 1: I|=P Therefore I|=C2 case 2: I|=~P Therefore I|=C1 Since one of these cases must hold, I |= C1 or I |= C2 Thus I |= C1 U C2 A non-deterministic entailment (satisfiability) procedure Res(S) if {} in S then return UNSAT choose C1, C2 containing complementary literals such that resolve(C1,C2) not in S if no such pair, return SAT S = S U resolve(C1,C2) Examples propositional resolution proofs If the unicorn is mythical, then it is immortal. If it is not mythical, then it is an animal. If the uniforn is either immortal or an animal, then it is horned. Proved: the unicorn is horned. **Size-preserving converson to CNF Bad case for direct conversion to cnf: (P1 & P2 & P3) v (Q1 & Q2 & Q3) If each conjunction is of length n, what is number of clauses of result? n**2 Even worse: (P1 & Q1) v (P2 & Q2) v ... v (Pn & Qn) What is number of clauses? 2**n How to prevent blow up? Introduce new propositions! Show how this is done: Instead of distributing v over &: 1. Introduce a new proposition Ci for each conjunction 2. Add clauses making Ci equivalent to the corresponding conjunction 3. Replace original disjunction by disjunction of Ci Example: (P1 & Q1) v (P2 & Q2) v ... v (Pn & Qn) ~C1 v P1 ~C1 v Q1 ~P1 v ~ Q1 v C1 same for other i C1 v C2 v ... Cn Explain relationship between original and augmented theory: They are not *quite* equivalent because new theory contains extra propositions. However: New |= Old And New is UNSAT iff Old is UNSAT and for any sentence S not containing the new propositions, New |= S iff Old |= S **Proof of completeness of propositional resolution Theorem: A set S of clauses is unsatisfiable iff there is a deduction of the empty clause from S. Correctness is <---, and completeness is ---> Suppose S is unsat. We will build a binary tree whose nodes "split" on the truth value assigned to a proposition. Thus: - each leaf is an interpretation - each internal node is a *partial* interpretation At each leaf, all the clauses must be false, otherwise there would be a satisfying interpretation. Put each clause on the highest node in the tree where it is false. The result is an (upside down) resolution proof of the empty clause! Example: P, ~P v Q, ~P v ~Q Create tree P/\~P / [P] Q/\~Q [~P,~Q] [~P,Q] 4.2 Conversion of universally-quantified formulas 1. Eliminate => and <=> 2. Move in ~ 3. Rename quantified variables, so all are distinct 4. Move out quantifiers 5. Distribute & over V 6. Skolemization: replace existentially-quantified variables by a new FUNCTION symbol, whose arguments are all the universally quantified variables to its left Example: Everyone who loves everyone loves someone who loves no one. A x . (A y . L(x,y)) => E z . L(x,z) & A w . ~L(z,w) **Relation of a formula to its Skolemization Is the converted formula EQUIVALENT to the original? No, because of the new function symbols. However, as in the case with introducing new propositions, they are closely linked: Skolem Formula |= Original Formula Skolem Formula is UNSAT iff Original Formula is UNSAT and for any sentence S not containing the skolem functions, New |= S iff Old |= S Class on 10/5 begins here: Most general unifier algorithm (Sec. 4.3.6) ** First-order resolution: Need to UNIFY the complementary literals, they might not be IDENTICAL. MGU(x,y,THETA): if THETA = FAIL then return FAIL if x = y return THETA if x is a variable then if x appears in y then return FAIL THETA = THETA U {x/y} if y is a variable then if y appears in x then return FAIL THETA = THETA U {y/x} /* x and y must both be functional terms */ if head(x) != head(y) then FAIL for x' in body(x) and y' in body(y) THETA = MGU(x,y,THETA) if THETA = FAIL return FAIL return THETA MGU(Knows(John,x), Knows(John, Jane)} MGU(Knows(John,x), Knows(y, Bill)} MGU(Knows(John,x), Knows(y, mother(y))} MGU(Knows(John,x), Knows(x,Elizabeth)} == fail Before computing Most General Unifier: rename variables in the two clauses if necessary to make them distinct. MGU(Knows(John,x), Knows(z,Elizabeth)} MGU(Knows(father(x),x), Knows(z,sister(John))) Resolve: [Knows(father(x),x)], [~Knows(z,sister(John)) v Happy(z)] [Happy(father(sister(John)))] MGU(Knows(father(x),x), Knows(z,sister(z))) FAILS! "Occurs check": block unification if you'd get a cycle in substitutions: Examples of FOL proofs Everyone who loves all animals is loved by someone Anyone who kills an animal is loved by no one Jack loves all animals Jack or Curiousity killed Tuna Tuna is a cat Did Curiousity kill the cat Tuna? Handling equality Note that MGU doesn't understand =. So: [A=B] [Friend(A,C)] should resolve with [~Friend(B,C)] How to handle? Explicit axioms: x=y & Friend(x,z) => Friend(y,z) Modify Resolution adding final case: if a unit clause [x=y] or [y=x] occurs, return THETA Incomplete. Really should create sets of equated literals. if x and y are in the same equivalence class, return THETA Still incomplete, since only takes information from unit clauses into account. Class on 10/7 begins here **Paramodulation If John is rich, his father is bill. Anyone's mother is married to their father. [~rich(john) v father(john)=bill] [Married(father(z),mother(z))] Paramodulation: for any terms x,y,z, where Unify(x,z)=THETA and z appears in the clause m1 v ... mn, l1 v ... v lk v x=y m1 v ... mn[z] ------------------------------------------- SUBST(THETA, l1 v ... v lk v m1 ... mn[y]) [~rich(john) v Married(bill,mother(john))] If John is rich, bill is married to his mother. Answer extraction Consider simplified example of "did Curiousity kill the cat?" Suppose we want to know WHO killed the cat. Want to "trace binding" of original existential quantifier in question (which becomes a universal). E x . Kill(x,Tuna) --> ~Kill(x,Tuna) v Answer(x) Stop when clause containing only Answer is derived. Completeness of FOL Resolution The Herbrand Theorem Define Herbrand universe All the ground terms that can be constructed from the function symbols in the theory. (Note: if no constants (0-ary function symbols), add one.) Define Saturation (of a clausal theory) All ground (variable free) clauses that can be created by subsituting some set of ground terms for the variables in an FOL CNF theory. Define Herbrand base: the saturation of a FOL CNF theory by its Herbrand Universe. Notation: H(S) Herbrand theorem: if a set S of clauses is unsatisfiable, then there is a finite subset of its Herbrand base H(S) that is unsatisfiable. Completeness of resolution for FOL based on LIFTING LEMMA: C1, C2 FOL clauses C1', C2' ground instances if C' in resolve(C1', C2'), then exists C in resolve(C1,C2) such that C' is a ground instance of C. Proof that FOL is not decidable Completeness means that if something is entailed by (is a theorem of) a theory, there exists a resolution proof. You can exhaustively search for longer and longer proofs until one is found. So, FOL is at least semi-decidable. If the query is not a theorem, resolution might run forever, generating longer and longer clauses with larger and larger terms -- infinitely many different clauses! Is there a proof system that is guaranteed to tell us that something is NOT a theorem? I.e., is FOL decidable? No! You can reduce the Halting Problem to that of determining if a formula is a theorem. Proven by Alonzo Church (1936) and Alan Turing (1937). Idea: encode a Turning machine in FOL. E.g. FSM state of Turning machine = {S1, ...., Sn, HALT} tape symbols = {A, B, C, SOT, EOT} use functions B, N to concatenate symbols tape: V a b c b a c tape to left of head B(b, B(a, sot)) tape to right of head N(b, N(a, N(c, eot))) Config(state, left_of_head, head, right_of_head) Initial configuration Operation of machine: if you read "A" in state s1, replace it with "B", go to state s3, and move head right: Config(S1, l, A, N(x,y)) => Config(S3, B(A,l), x, y) Halting: prove E l,h,r . Config(HALT, l, h, r)