# Theorem Prover Notes

## General Interest Sites

• Stanford Encyclopedia of Logic Technology

The Stanford Encyclopedia of Logic Technology is a compendium of information about logic technology. It includes theoretical material, an index to currently available technology, and a survey of applications. It includes pointers to relevant tutorials, publications, and web sites. And, it includes information about people, organizations, and conferences concerned with the development, deployment, and application of logic technology.

• Automatic Theorem Prover Repository

A repository of documentation, problem libraries, and systems for theorem proving and automated reasoning.

## Theorem Proving Systems

• EPILOG

Epilog is a library of Common Lisp subroutines for use in programs that manipulate information encoded in Standard Information Format (SIF), a variant of first order predicate calculus. It includes translators to convert expressions from one form to another, pattern matchers of various sorts, subroutines to create and maintain SIF knowledge bases, and a sound and complete inference procedure based on model elimination.

The inference procedure used in Epilog is based on a technique called model elimination. The procedure closely resembles that of Prolog; but, unlike that that of Prolog, the procedure used in Epilog is sound and complete for the entire language, i.e. all consequences the system derives are correct and it can derive all correct consequences of the information it is given.

SIF, the language supported by Epilog, is a proper subset of KIF (Knowledge Interchange Format), i.e. all expressions in SIF are expressions in KIF, but not all KIF expressions are expressions in SIF. Despite this subset relationship, SIF is fully expressive, i.e. for any set of KIF sentences, there is an equivalent set of SIF sentences. Thus, using the subroutines in Epilog, it is possible to build a sound and complete inference procedure for all of KIF.

Epistemics is providing the current version of Epilog free of charge for non-commercial use only. Do not redistribute.

• DTP

DTP (Don's Theorem Prover) is an inference engine written by Don Geddis for first-order predicate calculus, and it specializes in domain-independent control of reasoning. Vishal Sikka recommends it as an easy-to-use, easy-to-modify, stripped-down theorem prover.

• FRAPPS

FRAPPS (Framework for Resolution-based Automated Proof Procedures) is a portable resolution theorem-prover written in Common Lisp.

It facilitates the construction of a wide variety of resolution-based deductive systems. FRAPPS offers the basic functionality necessary to build such systems, freeing users from low-level implementation concerns. It is not intended for use in the construction of high-performance theorem provers, but rather to provide a modular and customizable system useful for rapid prototyping and experimentation in teaching and research. An extension to FRAPPS, called "Hooked on FRAPPS" or "Constraints in FRAPPS" enables the introduction of specialized unification procedures and constraints.

• PTTP - A Prolog Technology Theorem Prover by Mark E. Stickel

Prolog is not a full theorem prover for three main reasons:

1. It uses an unsound unification algorithm without the occurs check.
2. Its inference system is complete for Horn clauses, but not for more general formulas.
3. Its unbounded depth-first search strategy is incomplete. Also, it cannot display the proofs it finds.

The Prolog Technology Theorem Prover (PTTP) overcomes these limitations by

• transforming clauses so that head literals have no repeated variables and unification without the occurs check is valid; remaining unification is done using complete unification with the occurs check in the body;
• adding contrapositives of clauses (so that any literal, not just a distinguished head literal, can be resolved on) and the model- elimination procedure reduction rule that matches goals with the negations of their ancestor goals;
• using a sequence of bounded depth-first searches to prove a theorem;
• retaining information on what formulas are used for each inference so that the proof can be printed.

PTTP's high inference rate is achieved at the cost of not allowing more flexible search strategies or elimination of redundancy in the search space by subsumption. Although PTTP is one of the fastest theorem provers in existence when evaluated by its inference rate and performance on easy problems and it has been used to solve reasoning problems in planning and natural-language- understanding systems effectively, its high inference rate can be overwhelmed by its exponential search space and it is unsuitable for many difficult theorems.

The Otter theorem prover developed at Argonne National Laboratory has been quite successful at proving difficult theorems that are intractable for PTTP. Subsumption, demodulation, and weighting, all incompatible with PTTP, are crucial contributors to Otter's performance on difficult theorems.

• Other Systems, etc. and Research Sites

Last updated 6/29/95

Todd Neller,