Lecture 22

Logic Programming 


 - computation -> logic 
 - logic -> computation

 - Declarative 

     Logic programs do not express the control.

     Kowalski's view
           algorithm = logic + control
     Wirth's view
           algorithms + data structures = programs
 
 - Parallelism


1. Theoretical Background 

First Order Predicate calculus

  - propositions: claims, statements, and facts


  - operators (logical connectives):

        Name            Symbol
       -------------------------
        AND             ^  
        OR              v
        NOT             ~
        Implication     ->
        Equivalence     <->

  - constants: specific objects
  - variables: refer to unspecific objects

  - predicate: relation among objects

     > function: relations in which there in only one value for a given input.

  - quantifier:

        universal
        existential


  - The syntax of first-order logic in BNF

            Sentence :=   AtomicSentence 
                        | Sentence Connective Sentence 
                        | Quantifier Variable ... Sentence
                        | ~ Sentence
                        | (Sentence)

      AtomicSentence :=   Predicate(Term, ...) | Term = Term

                Term :=   Function(Term,...)
                        | Constant
                        | Variable

          Connective :=   ^ | v | -> | <->

          Quantifier :=   

            Constant := 

           Predicate := 

            Function := 


      Note: The precedence order (from hight to low) is ~, ^, v, ->, and <->
               


Inference rules:

  - Inference is to generate new sentences that are necessarily true, given that
    the old sentences are true. (entailment)



                         entails
            sentences  ---------------> sentence
               |                            |
               |                            |       representation
   ------------|----------------------------|---------------------
               |                            |       World
               |                            |
               v                            v 
             Facts   ------------------>  Facts
                         follows
  
   - rules (patterns)

      o Modus Ponens or Implication-Elimination

                a -> b, a
              ------------
                    b

      o And-Elimination

               a1 ^ a2 ^ ... ^ an
              --------------------
                       ai

      o And-Introduction

               a1, a2, ..., an
              -----------------
               a1 ^ a2 ^... ^ an

      o Double-Negation Elimination

               ~ ~ a
              -------
                 a

      o Unit Resolution

             a v b,  ~b
            ------------
                 b

      o Resolution

            a v b, ~b v c                          ~a -> b, b -> c
           ---------------  or equivalently       ------------------
               a v c                                   ~a -> c


      o Universal Elimination

            for_every v  a
          ------------------
            SUBST({v/g}, a)

           e.g., from for_every x Likes(x, IceCream), we can use the
            substitution {x/Ben} and infer Likes(Ben, IceCream).


      o Existential Elimination

            there_is v  a
          ------------------------
              SUBST({v/k}, a)

          e.g., from there_is x Kill(x, Victime), we can infer
            Kill(Murderer, Victim), as long as Murderer does not
            appear elsewhere in the knowledge base.

 
      o Existential Introduction

                  a
          -------------------------------------
           there_is v  SUBST({g/v}, a)

          e.g., from Likes(Jerry, IceCream) we can infer that
             there_is x Likes(x, IceCream).



      o Generalized Modus Ponens (GMP)


          For atomic sentences Pi, Pi', and Q, where there is a substitute
          theta such that subst(theta, Pi)=subst(theta,Pi'), for all i:
          
          P1', P2', ..., Pn', (P1 ^ P2 ^ ... ^ Pn) -> Q
        ------------------------------------------------
                  subst (theta,Q)

         e.g.,

          rainy(rocheseter), cold(rochester), rainy(x) ^ cold(x) -> snowy(x)
         -------------------------------------------------------------------
               snowy(rochester)




  Horn clauses (canonical form required by GMP)

     P1 ^ P2 ^ ... ^ Pn -> Q

     where P1, P2, ..., Pn and Q are atomic sentences (with no negation)

    e.g.,

       rainy(x) ^ cold(x) -> snowy(x).


  Unification: pattern matching (with variable substitution) to make two 
      sentences identical.

     e.g.,

       UNIFY(takes(john,cisc670), takes(y,z)) = {y/john, z/cisc670}
       
       the results of unification are substitutions. when variables are 
       given values, they are said to be instantiated.

     > A constant unifies only with itself.

     > Two structures unify iff they have the same functor and the same number
       of arguments, and the conrresponding arguments unify recursively.

     > A variable unifies with anything. If the other thing has a value, then
       the variable is instantiated. If the other thing is an instantiable
       variable, then two variables are associated in such a way that if either
       is given a value later, that value will be shared by both.    

     e.g., 

      UNIFY(knows(John,x), knows(x,Jane)) = ? {x/John, x/Jane}

      where the unification fails because x can not take on the valus John and Jane
      at the same time. 
      the solution is to standardize apart the two sentences being unified:

         UNIFY(knows(john, x1), knows(x2, Jane)) = {x1/John, x2/Jane}

  GMP + Unification:

     Forward-Chaining

     Backward-Chaining


   - GMP is incomplete, i.e., there are sentences entailed by the knowledge base the
      proof using GMP cannot infer.

      e.g.,

          for_every x P(x) -> Q(x)
          for_every x ~p(X) -> R(X)
          for_every x Q(x) -> S(x)
          for_every x R(x) -> S(x)

      While we know this entails S(A), which is not reachable via GMP because 
      for_every x ~P(x) -> R(x) cannot be converted to Horn form.

   Godel's Theorem of Completeness:

      For first-order logic,

          if KB |= a then KB |- R a

    where R is a complete proof procedure. Such a R was given by Robinson in 1965.