Reductions for non-clausal theorem proving

This paper presents the TAS methodology(1) as a new framework for generating non-clausal Automated Theorem Provers. We present a complete description of the ATP for Classical Propositional Logic, named TAS-D, but the ideas, which make use of implicants and implicates can be extended in a natural manner to first-order logic, and non-classical logics. The method is based on the application of a number of reduction strategies on subformulas, in a rewrite-system style, in order to reduce the complexity of the formula as much as possible before branching. Specifically, we introduce the concept of complete reduction, and extensions of the pure literal rule and of the collapsibility theorems; these strategies allow to limit the size of the search space. In addition, TAS-D is a syntactical countermodel construction. As an example of the power of TAS-D we study a class of formulas which has linear proofs (in the number of branchings) when either resolution or dissolution with factoring is applied. When applying our method to these formulas we get proofs without branching. In addition, some experimental results are reported. (C) 2001 Elsevier Science B.V. All rights reserved.