One-Pass Tableaux for Computation Tree Logic

DOI10.1007/978-3-540-75560-9_5zbMath1137.03304OpenAlexW1551169644MaRDI QIDQ3498455

Pietro Abate, Rajeev Goré, Florian Widmann

Publication date: 15 May 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-75560-9_5

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items (13)

Invariant-free clausal temporal resolution ⋮ The Proof Theory of Common Knowledge ⋮ Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) ⋮ One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ A Refined Resolution Calculus for CTL ⋮ Syntactic cut-elimination for common knowledge ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ Syntactic Cut-elimination for Common Knowledge ⋮ Dual systems of tableaux and sequents for PLTL ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ Modal Logic S5 Satisfiability in Answer Set Programming ⋮ Efficient SAT-based minimal model generation methods for modal logic S5

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• A clausal resolution method for branching-time logic \(\text{ECTL}^+\)
• Automata-theoretic techniques for modal logics of programs
• Proceedings of the 1st international workshop on Symbolic model checking (SMC '99), as part of the 2nd federated logic conference (FLoC '99). Trento, Italy, July 6, 1999
• About cut elimination for logics of common knowledge
• Decision procedures and expressiveness in the temporal logic of branching time
• Cut-free common knowledge
• How to optimize proof-search in modal logics
• Temporal logic can be more expressive
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• BDD-based decision procedures for the modal logic K ★
• Optimizing description logic subsumption
• Clausal temporal resolution
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science

This page was built for publication: One-Pass Tableaux for Computation Tree Logic