 |
The
figure to the left shows the successful part of the search for
a proof of the assertion that Marcus hates Caesar. The
database is reiterated in yellow at the top of the figure. Then
you will notice the statement that Marcus does not
hate Caesar. Resolution theorem proving works by negating
the assertion that is to be proved, and trying to prove a contradiction...or
the empty set.
The
numbers refer to the item in the database which is "resolved"
with the expression. This procedure involves two syntactic rules.
One is substitution which is carried out by a process called
unification. You don't really want to know the details; but what
this process does is substitute, in a clever way, values for
variables. The Marcus/x2 at the top of the search represents
the substitution of Marcus for the variable x2. The other rule
is modus ponens although that may not be so obvious. You need
to remember that 'not p or q' is identical to 'p -> q'. Then
clearly if you have 'p', 'not p or q' you can write down 'q'.
That is what is going on in the figure to the left. And, if you
get rid of everything, represented by the white box in the figure
which represents the empty set, then you have a contradiction!
But, you can get rid of the contradiction by asserting the negation
of what you started with....which was the negation of what you
wanted to prove...therefore, you just proved it!
|
