2008/11/4 Lesson Plan

* Parsing with Prolog

- Go over genesis_semantics carefully

- Go over assignment: have students create examples and syntax trees for each of:

    # Compound sentences with sentence-level connectives:
    
        * Eve eats the apple and Adam sleeps.
        * Eve eats the apple or Adam sleeps.

    # Conditional statements, e.g.:
    
        * If Eve loves the snake then Adam eats the apple.
        * Adam eats the apple if Eve loves the snake.
    
    # Verb phrases that use "is" to describe the subject with either an
      adjective or noun phrase, e.g.:
    
        * Eve is happy.
        * The snake is Satan.
    
    # Passive voice, e.g.:
    
        * The apple is eaten.
        * The apple is eaten by Adam.
        * The apple is given to Adam by Eve.
    
- Interact with class to create a solution to compound sentences.
Here is my solution:

compound_sentence(Tokens, Rest, S, Wff) :-
    sentence(Tokens, Rest, S, Wff).

compound_sentence(Tokens, Rest, compound_s(S1, C, S2), [Operator, Wff1, Wff2]) -->
    sentence(Tokens, Rest1, S1, Wff1),
    connective(Rest1, Rest2, C, Operator),
    compound_sentence(Rest2, Rest, S2, Wff2).

------------------------------------------------------------------------------

Introduction to full FOL theorem proving.

FOL conjunctive normal form:

"Everyone who loves all animals is loved by someone"

all x . ( all y . animal(y) => loves(x,y) ) => exists y. loves(x,y)

1. Eliminate implications
2. Move ~ inward
3. Standardize variables (rename variables apart).
4. SKOLEMIZE.  Talk about skolem functions.  Why does this make sense?
5. DROP universal qualitifier, will be IMPLICIT
6. Distribute OR over AND

Discuss:

- What is the relationship between the original and the CNF formula?
  Are they exactly logically equivalent?
  NO, because of the skolem functions.
  So what is the relationship?
      The original formula is SATISFIABLE iff the CNF version is
      SATISFIABLE.
         Similarly for UNSAT.
  This means we can use CNF for PROOF BY REFUTATION.

- Can you create a non-CNF formula which is VALID, but its CNF version
  is NOT valid?  (Try something very trivial!)

      	1. all x . exists y . x=y
	2. all x . x=f(y)
	3. x=f(y)

2 Rules of inference:
      
1. FOL RESOLUTION RULE:

L1 v ... v Lk,    M1 v ... v Mn
-------------------------------
SUBST(THETA, L1 v ... v Li-1 v Li+1 v ... Lk v 
             M1 v ... v Mj-1 v Mj+1 v ... Mn )

where UNIFY(Li, ~Mj) = THETA

2. FACTORING: delete "rundundant" literals in a clause.  

Consider the clause:

( doctor(X) v doctor(henry) )

This means: Either everyone is a doctor, or Henry is a doctor.
Suppose it is not the case that henry is a doctor.  Then, it must
be the case that everyone is a doctor.  But this would mean that henry
is a doctor, a contradiction!  So this case cannnot hold.
Therefore, from
   ( doctor(X) v doctor(henry) )
one can conclude:
   ( doctor(henry) )

The general FACTORING rule is:

L1 v ... v Lk
-------------------------------
SUBST(THETA, L1 v ... v Lj-1 v Lj+1 v ... Lk)

where i<j and UNIFY(Li, Lj) = THETA

EXAMPLE FROM TEXTBOOK: 
1. Everyone who loves all animals is loved by someone.
2. Anyone who kills an animal is loved by no one.
3. Jack loves all animals.
4. Either Jack or Curiousity killed the cat, who is named Tuna.
5. Did Curiousity kill the cat?