An Overview of the Tecton Proof System,
Theoretical Computer Science, Special Issue on
``Formal Methods in Databases ans Software Engineering,''
(ed. V. Alagar), North-Holland Press,
Vol. 133, October, 1994, 307-339.
Deepak Kapur, David R. Musser and Xumin Nie
The Tecton Proof System is an experimental tool for constructing proofs of first order logic formulas and of program specifications expressed using formulas in Hoare's axiomatic proof formalism. It is designed to make interactive proof construction easier than with previous proof tools, by maintaining multiple proof attempts internally in a structured form called a proof forest; displaying them in an easy to comprehend form, using a combination of tabular formats, graphical representations, and hypertext links; and automating substantial parts of proofs through rewriting, induction, case analysis, and generalization inference mechanisms, along with a linear arithmetic decision procedure. Further development of the system is planned as part of an overall framework aimed at supporting the kind of abstractions and specializations necessary for building libraries of generic software and hardware components.