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.
A repository of documentation, problem libraries, and systems for theorem proving and automated reasoning.
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 (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 (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.
Prolog is not a full theorem prover for three main reasons:
The Prolog Technology Theorem Prover (PTTP) overcomes these limitations by
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.