@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

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: <user-mailing list, publications>

Pragmatics:  <strengths/weaknesses>

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:
   <list of major applications -- brief description of problem and result,
   pointer to more info>
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  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%