zbMATH — the first resource for mathematics

tascpl: TAS solver for classical propositional logic. (English) Zbl 1111.68655
Alferes, José Júlio (ed.) et al., Logics in artificial intelligence. 9th European conference, JELIA 2004, Lisbon, Portugal, September 27–30, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23242-7/pbk). Lecture Notes in Computer Science 3229. Lecture Notes in Artificial Intelligence, 738-741 (2004).
Summary: We briefly overview the most recent improvements we have incorporated to the existent implementations of the TAS methodology, the simplified $$\Delta$$-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.
For the entire collection see [Zbl 1056.68002].
MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
HeerHugo; tascpl
Full Text: