[This README: created in 1995. Contact info updated 5/20/2002. Updated for ANSI CL 7/14/2004.] _______________________________________________________________________________ INTRODUCTION Welcome to the Don Theorem Prover (DTP), version 3.00 DTP is an inference engine for first-order predicate calculus, and it specializes in domain-independent control of reasoning. Please send comments to Don Geddis at don@geddis.org _______________________________________________________________________________ IMPLEMENTATION The original code was developed under Franz Allegro CL 4.2.beta.0 on a Sun Sparc, written in Common Lisp of the CLtL2 era. Earlier versions were tested on MCL 2.0p2 (Apple Macintosh) and Lucid HP Common Lisp Rev. A.04.01 (HP-9000 Series 300/400). In 2004 the core code was revised to conform to ANSI Common Lisp. Some optional extensions require non-ANSI functions; these are most likely to work with the CMUCL implementation, as well as perhaps Franz Allegro. _______________________________________________________________________________ AVAILABILITY DTP is available on the World Wide Web (WWW) from http://don.geddis.org/dtp/ in the file dtp.tar.gz ANSI Common Lisp source code + logic puzzle examples This file contains directories which have been run through the unix "tar" program and then compressed with the GNU zip utility ("gzip"). _______________________________________________________________________________ DOCUMENTATION The postscript documentation is available in the same DTP directory: http://don.geddis.org/dtp/manual.ps.gz Also of interest may be my thesis, available as http://don.geddis.org/dtp/thesis.ps.gz Most of the functionality is shown in the examples in the logical theories, which are exercised by running the function (TEST-DTP). It is often useful to run some of those examples by hand, in particular after turning on full tracing output with a sequence like this: (SETQ *THEORY* ') (SETQ *TRACE* (POSSIBLE-VALUES '*TRACE*)) (PROVE ') Other new functions of interest include: (SETTINGS) Describes the state of the theorem prover options (POSSIBLE-SETTINGS) Describes the possible states of the options (SHOW ) Takes a proof object or an answer object and generates a postscript graph of the space _______________________________________________________________________________ VERSION Version history: 3.00 ANSI CL 2.13 Contact info, code simplification 2.12 Term simplification on answers (as well as literals) 2.11 Fixed pure literal elim + proc attachment interaction 2.10 Simplified "view" proof figures 2.09 Re-introduced forking conjunctions 2.08 Merged answers and reduction answers 2.07 Iteration, on subgoal and function depth 2.06 Simplified conjunction solving (removed forward inference) 2.05 TPTP Library tools 2.04 General "view" tool on proofs and answers 2.03 Reduction check at conjunct instead of subgoal 2.02 Depth limits and iteration (broken) 2.01 Corrected reduction inference combined with caching 2.00 Subgoaling inference system 1.00 Resolution-based inference system _______________________________________________________________________________ RECOMMENDED SYSTEMS There are two auxiliary systems that make DTP more useful. For constructing postscript graphs of the proof spaces, AT&T's "dot" program is required. This is available as one of the modules in the open source project "graphviz": http://www.research.att.com/sw/tools/graphviz/ Of course, some mechanism for viewing the output is also needed: either a postscript previewer like the unix utility "ghostview", or else a postscript printer. A large number of theorem proving examples can be found in the TPTP (Thousands of Problems for Theorem Provers) collection: http://www.cs.miami.edu/~tptp/ _______________________________________________________________________________