Volume 6: January - December 1996

Issue 6: December 1996


A-ordered tableaux

  • A-ordered tableaux
  • R. Hahnle and S. Klingenbeck Institut fur Logik, Komplexitat und Deduktionssysteme, Fakultat fur Informatik, Universitat Karlsruhe, 76128 Karlsruh e, Germany


    In resolution proof procedures refinements based on A-orderings of literals have a long tradition and are well investigated. In tableau proof procedures such refinements were only recently introduced by the authors of the present paper. In this paper we prove the following results: we give a completeness proof of A-ordered ground clause tableaux which is a lot easier to follow than the one published previously. The technique used in the proof is extended to the non-clausal case as well as to the non-ground case and we introduce an ordered version of Hintikka sets that shares the model existence property of standard Hintikka sets. We show that A-ordered tableaux are a proof confluent refinement of tableaux and that A-ordered tableaux together with well-known connection refinements yield an incomplete proof procedure. We introduce A-ordered first-order NNF tableaux, prove their completeness, and we briefly discuss implementation issues.

    Keywords: Theorem proving, semantic tableaux, A-orderings.

    Pages: 819 - 833

    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

    Last updated 08 Jan 97

    Part of the OUP Journals World Wide Web service.

    Copyright Oxford University Press, 1997