CMPS140, Winter 2012, Section 01: Lecture 14

We are studying two theorem-proving methods for FOL:
    Resolution
    Existential Graphs

EGs have the advantage that they do not require clausification.



I. PEIRCE's INFERENCE RULES:
   1.  Double circles  may be  removed
   2.  Any graph may be deleted if there is a higher order or equal copy.
   3.  A blank circle can blow up its entire context    including itself.
   4. Forall(x,P(x)) = (x (P[x]))  Therexists(x,P[x]) = x P[x].
   5. We can substitute for a variable in an ODD context.



NOTE:
    We will prove things by negating them and then deriving "circle" -
    the empty context on the sheet.

     Suppose existing database is:
        3. ~S or P
        4. ~U or S
        5. U
        6. ~W or R
        7. W
     We wish to prove: P and (Q or R).


IN EGS:
       Must derive contradiction from:
            (S (P)) (U (S)) U  (W (R))  W   (P ((Q ) (R)))
   kill w:   (S (P)) (U (S)) U  R W      (P ((Q ) (R)))
   kill u:   (S (P))  S U R W (P ((Q ) (R)).
   kill s:     P     S U R W (P ((Q) (R)))
   kill p:     P S U R W  (Q) (R)
   kill r:    P S U R W (Q) ()
     KABOOM!!!!



Unification:

     Four instances of P[x,f(y),B] are     Substitutions.
        P[z,f(w),B]  alphabetic variant   {w/y}
        P[x,f(A),B]  more specific        {A/y}
        P[g(z),f(A),B] more specific yet  {g(z)/x,A/y}
        P[C,f(A),B]  ground instance since no variables.
                                          {C/x,A/y}

     Two or more expressions unify if there is a substitution
     that make them identical.

     The most general-unifier (mgu) of a set of expressions is
     the "simplest" substitution that makes them all equal.
     The principle being employed is known as LEAST-COMMITMENT
     or MINIMAL ENTROPY. Do not create complexity that
     does not exist.

     EXAMPLE:
         Consider unifying {P[x,f(y),B] with P[x,f(B),B]}
         a possible unifier is {A/x, B/y} but this is not
         most general since B/y will suffice.

      Unification can also be taken on a larger scale
      of arbitrary pattern matching, such as matching
      two hypergraph representations of chess positions.



In 1965, J.A. Robinson provided a tremendous contribution to Traditional
AI by inventing resolution, clausification, unification and showing
that resolution is complete for first order logic.

Ironically, it is exactly this contibution which may have set AI back
a few years, since it avoided understanding the structure of
knowledge in terms of graphs and hypergraphs.

In fact, clausification, as powerful as it is, removes exactly the
high-level structure that is used by humans for efficient theorem-proving.
Since Existential Graphs do not require a clausification stage this structure
is retained.


Clausification goes through nine stages:
    1. Eliminate implication symbols
    2. Reduce scope of negation.
    3. Standardize Variables (each quantifier gets a unique one).
    4. Eliminate Existential Quantifiers
         through Skolemization which creates a function that produces
         "the object that exists".
    5. Move universal quantifiers to front.
    6. Convert to CNF.
    7. Eliminate universals.
    8. Eliminate and, by breaking into separate clauses.
    9. Rename variables. -- every variable must occur in at most one clause.


Unification can be done with a straight forward algorithm
which works on expressions
in a left-to-right fashion and never requires backtracking...


We gave the basis of the Unification Algorithm:
Let x and y be variables.
Let A and B be constants.
Let f(x1,x2,...,xn) and g(x1,...,xm) be functions.

Then we consider the following situations:
    x unifies with y: x/y or y/x.
    x with B:   x/B
    x with f(x1,...,xn): f(x1,....xn)/x provided x does not occur in any
    xi.
    A with B: No, unless A=B.
    A with f(x1,...,xn): No, in general. (but with some math a
                               unification might be possible.)
    f(x1,.....,xn) with g(y1,....,ym). No unless:
             f=g, n=m and there is a unifier of (x1,....,xn) with
             (y1,...yn). That is, unification is called recursively.

Moving left to right and propogating substitutions to the
right (and to previous substitutions) this algorithm will
find a most general unifier if one exists.

Examples:
     Find mgu of P(x,z,y),P(w,u,w),P(A,u,u)

     an answer: P(A,z,A}

     These do not unify:
        P(f(x,x),A) with P(f(y,f(y,A)),A)
         P(f(A),x) with P(x,A)}.

==================================================
Example:
   All elephants ate the cake.
   Ganesh is an elephant.
   Hence, there is something which Ganesh ate.

   In egs:
        (x E(x) (Ate(x,K)))
        E(G)
        negated goal:   (y Ate(G,y))

   proof:
       substitute G for x and delete and remove double neg.:
              Ate(G,K)
       substitute K for y:
                (Ate(G,K))

      former kills latter leaving: ()!
=================================================================