A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance

DOI10.1007/978-3-642-31365-3_42zbMath1358.68266OpenAlexW1514845090MaRDI QIDQ2908524

Christoph Weidenbach, Martin Suda

Publication date: 5 September 2012

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-31365-3_42

Mathematics Subject Classification ID

Temporal logic (03B44)

Related Items (6)

Unnamed Item ⋮ Unnamed Item ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Variable and clause elimination for LTL satisfiability checking ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking

This page was built for publication: A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance