Labelled superposition for PLTL

DOI10.1007/978-3-642-28717-6_31MaRDI QIDQ2891470zbMATH OpenOpenAlexFDO

Authors Martin Suda, Christoph Weidenbach

Publication date 15 June 2012

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11858/00-001M-0000-0024-03DC-B

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A PLTL-prover based on labelled superposition with partial model guidance
• Cut, invariant rule, and loop-check free sequent calculus for PLTL
• Propositional temporal proving with reductions to a SAT problem
• An efficient decision procedure for propositional projection temporal logic
• scientific article; zbMATH DE number 3974944

Cited in

(4)

• A PLTL-prover based on labelled superposition with partial model guidance
• A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic
• Labelled Clauses
• Variable and clause elimination for LTL satisfiability checking

This page was built for publication: Labelled superposition for PLTL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2891470)