A simplified clausal resolution procedure for propositional linear-time temporal logic

DOI10.1007/3-540-45616-3_7MaRDI QIDQ4412853zbMATH OpenFDO

Authors Anatoli I. Degtyarev, Michael Fisher, B. Konev

Publication date 17 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2381/23810085.htm, https://kclpure.kcl.ac.uk/portal/en/publications/d2dc90f3-57f7-4d0d-974b-189c4b3747ff

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Recommendations

• A clausal resolution method for CTL branching-time temporal logic
• The complexity of propositional linear temporal logics in simple cases
• The complexity of propositional linear temporal logics
• The complexity of propositional linear temporal logics in simple cases. (Extended abstract)
• The axiomatization of propositional linear time temporal logic
• scientific article; zbMATH DE number 67448
• scientific article; zbMATH DE number 4197947
• A clausal resolution method for branching-time logic \(\text{ECTL}^+\)
• A resolution calculus for the branching-time temporal logic CTL
• The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic

Cited in

(12)

• Partial cut elimination for propositional discrete linear time temporal logic
• Invariant-free clausal temporal resolution
• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• Algorithms for guiding clausal temporal resolution
• A clausal resolution method for CTL branching-time temporal logic
• Deduction-based decision procedure for a clausal miniscoped fragment of FTL
• Propositional temporal proving with reductions to a SAT problem
• scientific article; zbMATH DE number 1444742 (Why is no real title available?)
• scientific article; zbMATH DE number 4197947 (Why is no real title available?)
• Clausal temporal resolution
• Simplifying inductive schemes in temporal logic
• Variable and clause elimination for LTL satisfiability checking

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: A simplified clausal resolution procedure for propositional linear-time temporal logic

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