Volume 7: January - December 1997

Issue 5: October 1997

Abstract


A description of the tableau method using abstract state machines

  • A description of the tableau method using abstract state machines
  • E. Borger and PH. Schmidt1

    Dipartimento di Informatica, Universita di Pisa, Corso Italia 40, I 56125 Pisa, Italy. E-mail: boerger@DI.UniPi.it and 1Institute for Logic, Complexity and Deductive Systems, Department of Computer Science, University of Karlsruhe, D-76128 Karlsruhe, Germany. E-mail: pschmitt@ira.uka.de

    ABSTRACT

    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.

    Pages: 659 - 681

    Part of the OUP Journal of Logic and Computation WWW service


    General Information

    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.