and E. Borger PH. Schmidt 1 Dipartimento di Informatica, Universita di Pisa, Corso Italia 40, I 56125and Pisa, Italy. E-mail: boerger@DI.UniPi.it 1Institute for Logic, Complexity and Deductive Systems, Department of Computer Science, University of Karlsruhe, D-76128 Karlsruhe, Germany. E-mail: firstname.lastname@example.org
Starting from the textbook formulation of the tableau calculus we give an operational description of the tableau method in terms of abstract state machines at various levels of refinement ending after four stages at a specification that is very close to the lean TAP implementation of the tableau calculus in PROLOG. Proofs of correctness and completeness of the refinement steps are given.
Keywords: Theorem proving, formal specification, tableau method, programme verification.
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Part of the OUP Journals World Wide Web service.
Last modification: 24 Oct 1997
Copyright© Oxford University Press, 1997.