tascpl: TAS Solver for Classical Propositional Logic

13 years 3 months ago
tascpl: TAS Solver for Classical Propositional Logic
We briefly overview the most recent improvements we have incorporated to the existent implementations of the TAS methodology, the simplified ∆-tree representation of formulas in negation normal form. This new representation allows for a better description of the reduction strategies, in that considers only those occurrences of literals which are relevant for the satisfiability of the input formula. These reduction strategies are aimed at decreasing the number of required branchings and, therefore, control the size of the search space for the SAT problem. 1 Overview of TAS TAS denotes a family of refutational satisfiability testers for both classical and non-classical logics which, like tableaux methods, also builds models for non valid formulas. So far, we have described algorithms for classical propositional logic [6,1], finite-valued propositional logics [3] and temporal logics [2]. The basis of the methodology is the alternative application of reduction strategies over formul...
Manuel Ojeda-Aciego, Agustín Valverde
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Authors Manuel Ojeda-Aciego, Agustín Valverde
Comments (0)