Lesson Plan 10/23

First-order inference: Unification and Lifting
Introduction to Prolog.

-------------------------------------
First-order inference: Unification and Lifting
-------------------------------------

A x . man(x) => mortal(x)
man(socretes).
 therefore: mortal(socretes).

In propositional logic: would have to instatiate the axioms over the set of all men
-- billions of people!
Instead: want to determine just what to substitute for x that is needed to prove
mortal(socretes).

In this case, it is easy: substitute socretes for x, write this as {x/socretes}

Two literals L1 and L2 UNIFY if there a substition THETA such L1 THETA = L2 THETA
In this case:
        motal(socretes) {x/socretes} = mortal(x) {x/socretes}

If two literals unify, they have a MOST GENERAL UNIFIER (substitution)

Say: L1 = Loves(x, mother(x))
     L2 = Loves(John, y)

What is substitution that makes L1 and L2 the same?
     {x/John, y/mother(John)}a           

Can generalize Modus Ponens to use unification:

   p1', p2', ..., pn', (p1 & p2 & ... & pn => q)
   ---------------------------------------------
                      q THETA

*if* there is a subsitution THETA such that
    p1' THETA = p1
    p2' THETA = p2 
    ...
    p3' THETA = p3

Details of the unification (MGU) algorithm:
Works on LISP notation.
Singleton: a constant, predicate, or variable.

Unify(x, y, THETA) 
// given partial substitution THETA, return a substition that
// makes x and y the same

  if (x and y are singletons and x=y) then return THETA;
  if (x is a variable) then 
     if there is a substitution x/z in THETA then
	return Unify(z,y,THETA)
     else
	return THETA U {x/y};
  if (y is a variable) then 
     if there is a substitution y/z in THETA then
	return Unify(x,z,THETA)
     else
	return THETA U {y/x};
  if (x or y is a singleton) then FAIL;
  // so both x and y are lists, the first element of the
  // list is either a predicate or a functor
  if ( first(x) != first(y) ) then fail
  for each argument a1,...,an in x and a1',...,an' in y do:
      THETA = Unify(ai,ai', THETA);
  return THETA
end.

--------------------------------------------------
Inference in Prolog

So, how to build a reasoning system?  We'll start by just using the Modus Ponens
rule, even though it is not a complete rule for all of FOL.

But there IS an important case for which modus ponens IS complete:
modus ponens is REFUTATION COMPLETE for DEFINITE CLAUSES.

What are definite clauses?  These are formulas that 
- only has quantifiers at the beginning of the formula, and they must be UNIVERSAL
- a disjunction of literals, where exactly ONE of the disjuncts is POSITIIVE
- functors (function symbols) ARE allowed

Example of definite clauses:
A x. ~person(x) v ~female(x) v woman(x)
A x. (person(x) & female(x)) => woman(x)
A x . married(x) => loves(x, spouse(x))
married(adam)

Example of non-definite clauses:
A y E x . loves(x,y).
man(adam) v man(eve).
~man(eve).

Modus ponens can be use to create PROOFS in either a forward or backward direction.
Draw picture.

PROLOG can be viewed as either a DEFINITE CLAUSE THEOREM PROVING SYSTEM or as a
PROGRAMMING LANGUAGE.

PROLOG modifies definite clauses in severals ways:

- a special syntax: 
	- clauses are written as rules
	- quantifiers are not explicitly shown - instead, variables begin with a
        CAPITAL LETTER.
	- instead of & just write comma:

woman(X) :- person(X),  female(X).

- all distinct terms are assumed to refer to distinct individuals.  So the equality
  predicate can be implemented by simply checking that two terms can UNIFY:

adam = eve         	ALWAYS FALSE
X = eve     		ALWAYS TRUE, with X being UNIFIED with the constant eve
father(X) = adam	ALWAYS FALSE
father(X) = father(adam)	TRUE, X unifies with adam
X = father(Y)			TRUE, X unifies with father(Y)
cons(a,cons(b,nil)) = cons(X,cons(Y,Z))
		TRUE, unifies a with X, b with Y, Z with nil

- proofs are always created in a DEPTH FIRST, LEFT TO RIGHT order.
	- begin with a single positive literal to prove:
		? loves(adam, Y).
	- find the first clause where the POSITIVE part (HEAD) of the clause unifies 
		with the literal ***
		loves(X,spouse(X)) :- married(X).
	unify:
		loves(adam,spouse(adam)) :- married(adam).
	- recurse on each literal in the BODY
		married(adam) unifies with married(adam).
	- returns: Y = spouse(adam).

SUPPOSE the proof FAILS at any point to find a clause to unify with?  Then the Prolog
interpreter BACKTRACKS to the point *** and finds the NEXT clause with a unifiable head
instead.