PLOGHELP RESOLVE Kathryn Seifert September 1986 Teaching packages for resolution theorem proving Keywords: theorem proving, resolution, logic, predicate calculus CONTENTS - (Use 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