Increasing the efficiency of automated theorem proving
Gabriel Aguilera‐Venegas, Inma P. de Guzmán, Manuel Ojeda · Journal of Applied Non-Classical Logics · 1995
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 [12]). TAS-D++ works by using transformations of the syntactic trees of the formulas and, as tableaux and matrix style provers [6, 15, 16], it is Gentzen-based. Its power is mainly based in the efficient extraction of implicit information in the syntactic trees (in difference with the standard ATPs via refutation) to detect both: • simultaneously unsatisfiable or equivalent formulas to that being studied • valid, unsatisfiable, equivalent or equal subformulas. TAS-D++ is sound and complete and, moreover, it is a method that generates countermodels in a natural way.