zbMATH — the first resource for mathematics

A PLTL-prover based on labelled superposition with partial model guidance. (English) Zbl 1358.68266
Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 537-543 (2012).
Summary: Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this observation to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.
For the entire collection see [Zbl 1245.68010].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B44 Temporal logic
PDF BibTeX Cite
Full Text: DOI