PLOGHELP RESOLVE                         Kathryn Seifert  September 1986

Teaching packages for resolution theorem proving

Keywords: theorem proving, resolution, logic, predicate calculus


CONTENTS - (Use <ENTER> g to access sections)

 -- LIBRARY RESOLUTION PROGRAMS
 -- DEFINITION
 -- CLAUSAL FORM
 -- THE RULE OF RESOLUTION
 -- UNIFICATION
 -- RELATED DOCUMENTATION


-- LIBRARY RESOLUTION PROGRAMS ----------------------------------------

There are two library files, LIB * RESOLVE1 and LIB * RESOLVE2, which
contain simple resolution programs.  These programs can be run to
demonstrate the principal of resolution theorem proving.  They can also
provide the basis for the writing of more complex theorem proving
programs.

These programs work on a database of clauses in the format given by
TEACH * RESOLUTION.  LIB * CLAUSIFY (see PLOGHELP * CLAUSIFY) can be
used to translate predicate calculus propositions into clausal form (see
below).

-- DEFINITION ---------------------------------------------------------

"Resolution" is a rule of inference which can be used to find proofs in
the predicate calculus.  The proof method is a form of 'reductio ad
absurdum'; i.e. given a set of formulae or axioms, the negation of the
theorem we are trying to prove is added to this set and then an attempt
is made to derive a contradiction.  If the attempt succeeds, then we
have proved the theorem.

-- CLAUSAL FORM -------------------------------------------------------

Resolution applies only to a restricted class of formulae: those in
clausal form.  Therefore, if the theorem is given a set of predicate
calculus formulae to work with, these formulae must first be translated
into clauses.  A "clause" in this context is a disjunction of literals,
where each literal is either a proposition or a negated proposition,
e.g.
            programmer(joan) V ~employed(joan).

Clauses should contain no quantifiers.  All free variables in the
clauses will be universally quantified, and existentially quantified
variables will replaced by "skolem functions" and "skolem constants".

-- THE RULE OF RESOLUTION ---------------------------------------------

The rule of resolution is quite simple: if we have two clauses, one
containing the literal P and one containing the literal ~P, where C1 and
C2 are the respective remaining disjoined clauses, we can deduce C1 V
C2. The initial clauses are called the parent clauses of the resolvant
and P, ~P are called complementary literals.  If both C1 and C2 are
empty, then we can derive the empty clause.  This is the goal of
resolution, as the derivation of the empty clause indicates that a
contradiction has been discovered.  Therefore, when resolving two
clauses together, having C1 or C2 empty is fortuitous, as the resolvent
will be shorter than either of the parent clauses.

-- UNIFICATION --------------------------------------------------------

Sometimes, the two parent clauses may not have complementary literals,
but it may be possible to apply substitutions to each of the clauses so
that the resulting clauses do contain complementary literals.  This
substitution is performed using a process called "unification" (see
TEACH * RESOLUTION).

-- RELATED DOCUMENTATION ----------------------------------------------

PLOGHELP * CLAUSIFY
 Library file for changing predicate calculus formulae to clausal form

TEACH * RESOLUTION
 Tutorial introduction to resolution and relation of logic to Prolog