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...

• Type: Conference
• Year: 2004
• Where: JELIA
• Authors: Manuel Ojeda-Aciego, Agustín Valverde
• Keywords: Artificial Intelligence, JELIA 2004, Logics, Propositional Logics, Reduction Strategies