Reductions for non-clausal theorem proving

This paper presents the TAS methodology(1) as a new framework for generatin g non-clausal Automated Theorem Provers. We present a complete description of the ATP for Classical Propositional Logic, named TAS-D, but the ideas, w hich make use of implicants and implicates can be extended in a natural man ner 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 re write-system style, in order to reduce the complexity of the formula as muc h as possible before branching. Specifically, we introduce the concept of c omplete reduction, and extensions of the pure literal rule and of the colla psibility 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 linea r proofs (in the number of branchings) when either resolution or dissolutio n with factoring is applied. When applying our method to these formulas we get proofs without branching. In addition, some experimental results are re ported. (C) 2001 Elsevier Science B.V. All rights reserved.