@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: Deductive Tableau Keywords: first-order, induction, program extraction Name: Deductive Tableau Keywords: first-order, induction, program extraction Description: Semantics: classical first-order logic Built-in theories: equality, integers, tuples, trees Deductive machinery: nonclausal resoltuion, stepwise and well-founded induction, skolemization, simplification, and rewriting Dynamics: Proofs developed via a graphical user interface. New theories may be introduced by the user. Persistence: The system retains theories, proofs, and partial proofs. The Deductive Tableau system is based on the logical framework presented in Manna and Waldinger's textbooks (see below). It has been used both as courseware for classes based on the book and as a tool for research in program synthesis, planning, and database management. The system exploits the MacIntosh user interface. Proofs are displayed on the screen in a two-dimensional tableau format. The user indicates with the cursor what rule to apply next and to what subexpressions it is to be applied; the system presents the result to the user, who may accept or reject it. Explanations for each step are displayed in a separate column. The user may also invoke an automatic mode. In an experimental version, programs can be extracted from sufficiently constructive proofs. Contact persons: Ron Burback burback@neon.stanford.edu User group: Pragmatics: Documentation: `Using the Deductive Tableau System,' by Burback, Manna, Waldinger, et al.; See also Manna and Waldinger, `The Logical Basis for Computer Programming' (Addison-Wesley, Volume I, 1985; Volume II, 1990) and `The Logical Foundations of Computer Programming' (Addison-Wesley, 1993, to appear). Applications: Educational tool Extensions/enhancements: Resource requirements: Macintosh Where-to-get-it: An interactive theorem-proving system linked to this work has been implemented on the Apple Macintosh and is available for classroom use. Distributed by: Chariot Software Group, 3659 India Street, Suite 100C, San Diego, CA 92103. 1-800-CHARIOT. California: 619 298-0202. For more information, write to the following address: Tableau Deductive Systems, P.O. Box 9779, Stanford, California 94309. [info source/date] email to theorem-provers mailing list end 91 and flier 92 zm April 92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%