On the relative merits of path dissolution and the method of analytic tableaux (Q1331929)

In J. Assoc. Comput. Mach. 40, No. 3, 504-535 (1993; Zbl 0785.68083), the authors introduced a path dissolution as an inferencing mechanism that generalizes the method of analytic tableaux. The present paper examines the tableau paradigm and presents several results demonstrating that tableau deductions can be substantially speeded up by applying the path dissolution technique. Section 2 briefly reviews this technique. The tableau methods are casted in the framework of semantic graphs. Section 3 describes in detail the techniques for speeding up tableau deductions. The various speedup theorems presented are directly implementable into any tableau prover, and reveal a unifying concept that can be used: unit dissolution. Section 4 discusses the influence of conjunctive and disjunctive factoring on tableau and path-dissolution methods. S. Cook and R. Reckhow (1974) described a class of formulas that are intractable for analytic tableaux but can be handled in linear time by resolution. The authors show that the appropriate use of factoring as a preprocessing step in the standard tableau (and dissolution) methods provides linear time proofs for the Cook-Reckhow class of formulas. A final remark: the way dissolution generalizes the tableau method, though applied only to the propositional case here, is clearly applicable to the structure of proof trees in first-order tableau operations.