and R. Hahnle 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.
Theorem proving, semantic tableaux, A-orderings.
Part of the OUP Journal of Logic and Computation WWW service
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