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".