A-ordered tableaux

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 previous one. 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 Hintikks sets. We show that
A-ordered tableaux are a proof confluent refinement of tableaux and
that A-ordered tableaux together with the connection refinement
yield an incomplete proof procedure. We introduce A-ordered
first-order NNF tableaux, prove their completeness, and we briefly
discuss implementation issues.