H ? « ‹ ← → › »

Language peer sets for DTP:
United States↑
United States/1994↑
Designed 1994 ↑
1990s languages ↑
Fifth generation↑
Post-Cold War↑

DTP(ID:3670/dtp001)

alternate simple view
Country: United States
Designed 1994
Published: 1994

for Don's Theorem Prover

General theorem prover with domain-independent control of inference, running on Common LIsp

Don Geddis  Computer Science Department Stanford University 1994

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.

Structures:
Related languages
Common LISP → DTP   Based on

Resources
Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder