In this work a new Automated Theorem Prover (ATP) via refutation for classical logic and which does not require the conversion to clausal form, named TAS-D++, is introduced. The main objective in the design of this ATP was to obtain a parallel and computationally efficient method naturally extensible to non-standard logics (concretely, to temporal logics, see [8]).
TAS-D++ works by using transformations of the syntactic trees of the formulae and, as tableaux and matrix style provers [3, 11, 12], it is Gentzen-based. Its power is mainly based in the efficient extraction of implicit information in the syntactic trees to detect valid, unsatisfiable, equivalent or equal subformulae (in difference with the standard ATPs via refutation which have a general algorithm for all formulae). TAS-D++ is sound and complete and, moreover, it is a method that generates countermodels in a natural way. This method is implemented in [1].