2008/11/4 Lesson Plan

Inference in First Order Logic:

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

Applications of FOL theorem proving:
- Mathematics
- Hardware and software verification
- Knowledge bases

Mathematics example:
Prove that if a relationship is symmetric, transitive, and total, then it is
reflexive.

S1: A x A y P(x,y) => P(y,x)
S2: A x Ay Az (P(x,y)&P(y,z))=> P(x,z)
S3: Ax Ey P(x,y)

Prove: A x P(x,y)

*******************************

Constructive vs. Non-constructive Proofs:

Many proofs take the form of a QUERY: 
prove that E x . Q(x)  for some predicate or sentence Q.

If the proof actually gives a *particular value* for x, then it is CONSTRUCTIVE.

Compare:
KB = { cat(puff), cat(tuna) v cat(whiskers) }
E x cat(x)?
Consider the 2 different resolution proofs.  The one for 
x=puff is CONSTRUCTIVE, the one for tuna v whiskers is NOT.

How to ensure that we only get CONSTRUCTIVE answers?  One method: create a new
* answer predicate *.  Replace original goal
~cat(x)
with
~cat(x) v answer(x)
Now, you will never be able to get an empty clause.  The new stopping condition is
when you get a UNIT ANSWER CLAUSE.
So, in this case,
(answer(puff))

********************************

EQUALITY:  In FOL we might NOT want to make the assumption, as in Prolog, that every
different term refers to a different variable.  For example, we might want to say

   father(sam) = father(mary) = fred

One non-practical approach is to add formulas that define equlaity:
- equality refective, transitive, symmetric
- can substitute equals for equals in all predicates

Better approaches:

- Extend idea of unification: two terms are unifiable if they a "provably" equal.
    what could provably equal mean?
	- after evaluating arithmetic expressions
	- after putting arithemtic expressions in cannonical form
	- if ground terms appear in same EQUIVALENCE SET.

Equivalence set idea: Whenever a ground term is first generated, it is placed in its
own equivalence set.  Whenever a UNIT CLAUSE between two ground terms is generated,
e.g.
	fred = father(sam)
the two sets are combined, using the UNION-FIND algorithm.  NOTE: = is treated just
like a regular predicate otherwise.

EXAMPLE:



Equivalence sets are cheap to implement but not COMPLETE.  A complete method is
PARAMODULATION, a new rule of inference:

for any terms x, y, z where UNIFY(x,z) = THETA

l1 v ... lk v x=y,       m1 v ... v mn[z]
----------------------------------------------
SUBST(THETA, l1 v ... v lk v m1 v .... v mn[y])