CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

DTP: General theorem prover with domain-independent control of inference.

DTP (Don's Theorem Prover) is a sound and complete inference engine for first-order predicate calculus. It specializes in domain-independent control of inference. The intended audience is those who need a reliable black box for drawing conclusions and answering queries from a knowledge base of full first-order axioms. It was created to incorporate all the necessary search control knowledge; the database itself need have no search control at all, either explicit or implicit (e.g. rule or conjunct ordering). An ideal application, for example, would be as the back end to a machine learning program or mobile robot. Such systems have a hard enough time just discovering true things about their worlds, much less figuring out how to arrange that knowledge in a computationally tractable way. The philosophy in DTP is that the user need only be concerned about writing down true axioms, and all search control knowledge will be embedded in the inference engine. It includes some logic puzzle examples and a users manual.
Origin: []

Version: 2.4 (24-JUN-94) Requires: Common Lisp (CLtL2) Ports: It runs in Franz Allegro, Lucid, and Macintosh (MCL) Common Lisp. CD-ROM: Prime Time Freeware for AI, Issue 1-1 Author(s): Don Geddis Computer Science Department Stanford University Stanford, California 94305 Tel: 415-723-2273 Keywords: Authors!Geddis, Automated Reasoning, DTP, Inference Engines, Logic, Meta Reasoning, Reasoning!Automated Reasoning, Reasoning!Meta Reasoning, Resolution Theorem Proving, Search Control, Subgoaling, Theorem Proving References: ?
Last Web update on Mon Feb 13 10:27:28 1995