×

zbMATH — the first resource for mathematics

Propositional temporal proving with reductions to a SAT problem. (English) Zbl 1381.68277
Bonacina, Maria Paola (ed.), Automated deduction – CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38573-5/pbk). Lecture Notes in Computer Science 7898. Lecture Notes in Artificial Intelligence, 421-435 (2013).
Summary: We present a new approach to reasoning in propositional linear-time temporal logic (PLTL). The method is based on the simplified temporal resolution calculus. We prove that the search for premises to apply the rules of simplified temporal resolution can be re-formulated as a search for minimal unsatisfiable subsets (MUS) in a set of classical propositional clauses. This reformulation reduces a large proportion of PLTL reasoning to classical propositional logic facilitating the use of modern tools. We describe an implementation of the method using the CAMUS system for MUS computation and present an in-depth comparison of the performance of the new solver against a clausal temporal resolution prover.
For the entire collection see [Zbl 1264.68002].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03B44 Temporal logic
PDF BibTeX Cite
Full Text: DOI