CMU Artificial Intelligence Repository
DTP: General theorem prover with domain-independent control
of inference.
areas/reasonng/atp/systems/dtp/
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:
meta.stanford.edu:/pub/dtp/ [36.8.0.54]
meta.stanford.edu:/pub/papers/
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
AI.Repository@cs.cmu.edu