November 12 Logic * Truth tables A B | -A A->B -A->(A->B) ----+--------------------- T T | F T T T F | F F T F T | T T T F F | T T T * Rules of Inference for Propositional Logic - Idempotency fvf = f f^f = f - Commutativity fvg = gvf f^g = g^f f<->g = g<->f - Associativity (fvg)vh = fv(gvh) (f^g)^h = f^(g^h) - Absorption fv(f^g) = f f^(fvg) = f - Distributivity f^(gvh) = (f^g)v(f^h) fv(g^h) = (fvg)^(fvh) - Tautology fvg = f if f is a tautology f^g = g if f is a tautology - Unsatisfiability fvg = g if f is unsatisfiable f^g = f if f is unsatisfiable - Modus ponens: A, A=>B (antecedent, consequent) ------- B All men are mortal (Man => Mortal) Socrates is a man (Man) ---------------------------------- Socrates is mortal (Mortal) - And introduction: A, B ---- A^B - Or introduction: A - A, B, C, D, ... - And elimination: A^B^C^...^Z ----------- A - Double-Negation Elimination: ~~A --- A - Unit Resolution: A v B, ~B --------- A Today is either Tuesday or Thursday, Today is not Thursday ---------------------------------------------------------- Today is Tuesday - Resolution: A v B, ~B v C ~A => B, B => C ------------- --------------- A v C ~A => C Today is Tuesday or Thursday Today is not Thursday or tomorrow is Friday ------------------------------------------- Today is Tuesday or tomorrow is Friday * Propositional Logic vs. First-Order Predicate Calculus PL - only propositions (symbols representing facts) Only values True and False First-Order Logic includes: Objects: peoples, numbers, places, ideas (atoms) Relations: relationships between objects (predicates, T/F) father(fred, mary) Properties: properties of atoms (predicates, T/F) red(ball) Functions: father-of next, (any value in range) * FOPC * Syntax Constant symbols (Capitalized, Constants with no arguments) Interpretation must map to exactly one object in the world Predicates (can take arguments, True/False) Interpretation maps to relationship or property T/F value Function (can take arguments) Maps to exactly one object in the world * Definitions Term Anything that identifies an object Function(args) Constant (function with 0 args) Atomic sentence Predicate with term arguments Bunny(Bugs) Enemies(Wily_Coyote, Road_Runner) Married(Father_Of(Alex), Mother_Of(Alex)) Literals atomic sentences and negated atomic sentences Connectives ^, v, ->, <=>, ~ if connected by "^", conjunction (components are conjuncts) if connected by "v", disjunction (components are disjuncts) Quantifiers Universal Quantifier How do we express "All unicorns speak English" in PL? We have to specify proposition for each unicorn FORALL is used to express facts and relationships that we know to be true for all members of a group (objects in the world) A variable is used in the place of an object FORALL x, Unicorn(x) => SpeakEnglish(x) The domain of x is the world The scope of x is the statement following FORALL (sometimes in []) Same as specifying Unicorn(Uni1) => SpeakEnglish(Uni1) ^ Unicorn(Uni2) => SpeakEnglish(Uni2) ^ Unicorn(Uni3) => SpeakEnglish(Uni3) ^ ... Unicorn(Table1) => Table(Table1) ^ ... One statement for each object in the world We will leave variables lower case (sometimes ?x) Notice that x ranges over all objects, not just unicorns. A term with no variables is a "ground term" Existential Quantifier This makes a statement about some object (not named) THERE EXISTS x, Bunny(x) ^ EatsCarrots(x) means there exists some object in the world (at least one) for which the statement is true. Same as disjunction over all objects in the world. (Bunny(Bun1) ^ EatsCarrots(Bun1)) v (Bunny(Bun2) ^ EatsCarrots(Bun2)) v (Bunny(Bun3) ^ EatsCarrots(Bun3)) v (Bunny(Bun4) ^ EatsCarrots(Bun4)) v (Bunny(Bun5) ^ EatsCarrots(Bun5)) v ... (Bunny(Table1) ^ EatsCarrots(Table1)) v ... What about THERE EXISTS x, Unicorn(x) => SpeakEnglish(x) ? Means implication applies to at least one object in the universe. * Properties FORALL x ~P <=> ~EXISTS x P FORALL x P <=> ~EXISTS x ~P ~FORALL ~P <=> EXISTS x P ~FORALL x P <=> EXISTS x ~P FORALL x LovesWatermelon(x) <=> ~EXISTS x ~LovesWatermelon(x) (X => Y) <=> ~X v Y Prove with truth table. NOT TRUE: (X => Y) <=> (Y => X) This is a type of inference/learning that is not sound (abduction). Examples * All men are mortal FORALL x [Man(x) => Mortal(x)] * Socrates is a man. Man(Socrates) * Socrates is mortal Mortal(Socrates) Notice - if we could match Socrates with x, we could prove this statement using Modus Ponens. We would look at such a matching (unification) later. * All purple mushrooms are poisonous FORALL x [(Purple(x) ^ Mushroom(x)) => Poisonous(x)] * A mushroom is poisonous only if it is purple FORALL x [(Mushroom(x) ^ Poisonous(x)) => Purple(x)] * No purple mushroom is poisonous ~(EXISTS x [Purple(x) ^ Mushroom(x) ^ Poisonous(x)] * There is exactly one mushroom EXISTS x [Mushroom(x) ^ (FORALL y (NEQ(x, y) => ~Mushroom(y)))] Because exactly one is difficult, we can use EXISTS! x to denote exactly one object. * Every city has a dog catcher who has been bitten by every dog in town. Use City(1), DogCatcher(1), Bit(2), Lives(2) FORALL a, b [City(a) => EXISTS c {DogCatcher(c) ^ (Dog(b) ^ Lives(b,a) => Bit(b,c))}] * No human enjoys golf FORALL x [Human(x) => ~Enjoys(x, Golf)] * Some professor that is not a historian writes programs EXISTS x [Professor(x) ^ ~Historian(x) ^ Writes(x, Programs)] * Every boy owns a dog FORALL x EXISTS y [Boy(x) => Owns(x, y)] EXISTS dog FORALL x [Boy(x) => Owns(x, y)] Do these mean the same thing? * Higher-order Logic FOPC quantifies over objects in the universe. Higher-order logic quantifies over relations and functions as well as objects. * All functions with a single argument return a value of 1. FORALL x, y [Equal(x(y), 1)] * Two objects are equal iff all properties applied to them are equivalent. FORALL x, y [(x=y) <=> (FORALL p[p(x) <=> p(y)])] Notice that we use "=" as a shorthand for equal. equal means they are in fact the same object. * Example Proof The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American. Prove: West is a criminal. Known: 1) FORALL x, y, z [(American(x) ^ Weapon(y) ^ Nation(z) ^ Hostile(z) ^ Sells(x,z,y)) => Criminal(x)] It is a crime for an American to sell weapons to hostile nations 2) EXISTS x Owns(Nono, x) ^ Missile(x) Nono has some missiles 3) FORALL x Owns(Nono,x) ^ Missile(x) => Sells(West,Nono,x) All of its missiles were sold to it by Colonel West 4) FORALL x Missile(x) => Weapon(x) 5) FORALL x Enemy(x,America) => Histile(x) 6) American(West) 7) Nation(Nono) 8) Enemy(Nono,America) 9) Nation(America) Proof: 10) Owns(Nono,M1) ^ Missile(M1) 2 ^ Existential Elimination Existential Elimination EXISTS v [] Substitute k for v anywhere in sentence, if k does not appear in [] k is a constant (term with no arguments) (Skolemization) 11) Owns(Nono,M1) 10 ^ And-Elimination 12) Missile(M1) 10 ^ And-Elimination 13) Missile(M1) => Weapon(M1) 4 ^ Universal Elimination Universal Elimination FORALL v [] If true for universal variable v, true for a ground term (term with no variables g) 14) Weapon(M1) 12, 13, Modus Ponens 15) Owns(Nono,M1) ^ Missile(M1) => Sells(West,Nono,M1) 3 ^ Universal Elimination 16) Sells(West,Nono,M1) 10, 15, Modus Ponens 17) American(West) ^ Weapon(M1) ^ Nation(Nono) ^ Hostile(Nono) ^ Wells(West,Nono,M1) => Criminal(West) 1 ^ Universal Elimination (x West) (y M1) (z Nono) 18) Enemy(Nono,America) => Hostile(Nono) 5 ^ Universal Elimination 19) Hostile(Nono) 8, 18, Modus Ponens 20) American(West) ^ Weapon(M1) ^ Nation(Nono) ^ Hostile(Nono) ^ Sells(West,Nono,M1) 6, 7, 14, 16, 19, And-Introduction 21) Criminal(West) 17, 20, Modus Ponens Another rule: Existential Introduction If [..g..] true (where g is ground term) then EXISTS v [..v..] true (v is substituted for g) * Generalized Modus Ponens If we have a rule p1 ^ p2 ^ p3 ^ p4 ^ p5 ^ ... ^ pn => q Each p involves universal / existential quantifiers And we have each antecedent clause p1(x) p2(y) ... pn(z) And we can find a way to UNIFY the variables Then we can infer q Missile(x) ^ Owns(Nono,x) => Sells(West,Nono,x) Missile(M1) Owns(Nono,M1) Must make sure that instantiations of x are the same This process is "unification".