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: ()!

=================================================================