This page represents the current state of an ongoing effort to collect information about existing automated reasoning systems. One objective is to provide concise useful information for people who have need for such a system and don't want to `roll their own'. Another objective is to provide a single place where information about existing systems can be accessed, thus providing an overview of the state of the art.
Despite Prolog's logic heritage and its use of theorem-proving unification and resolution operations, Prolog fails to qualify as a full general-purpose theorem-proving system. There are three main reasons: (1) many Prolog systems use an unsound unification algorithm, (2) Prolog's unbounded depth-first search strategy is incomplete, and (3) Prolog's inference system is not complete for non-Horn clauses. Nevertheless, Prolog is quite interesting from a theorem-proving standpoint because of its very high inference rate as compared to conventional theorem-proving programs. The objective of the Prolog Technology Theorem Prover (PTTP) is to overcome the deficiencies while retaining as fully as possible the high performance of well-engineered Prolog systems.
* Automated Reasoning Database at Stanford. * The TPTP Home Page. * QED Home page. * ORA Bibliography of Automated Deduction * Tomás Uribe's automated deduction page. * Logical Frameworks Page. * Formal Methods Library at Oxford. * The Mizar Home Page. * Association for Automated Reasoning (AAR) * Conference on Automated Deduction (CADE) * Journal of Automated Reasoning (JAR)