 |
    |
Propositional Temporal Proving with Reductions to a SAT Problem
Richard Williams and Boris Konev
Department of Computer Science, University of Liverpool, Liverpool L69 7ZF, UKR.M.Williams1@liv.ac.uk
Konev@liv.ac.uk
Abstract. 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.
LNAI 7898, p. 421 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013