A resolution calculus for the branching-time temporal logic CTL
From MaRDI portal
Publication:5410337
DOI10.1145/2529993zbMath1287.03033OpenAlexW2080448334MaRDI QIDQ5410337
Lan Zhang, Ullrich Hustadt, Clare Dixon
Publication date: 16 April 2014
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2529993
Related Items (6)
Ordered Resolution for Coalition Logic ⋮ To be fair, use bundles ⋮ Computing sufficient and necessary conditions in CTL: a forgetting approach ⋮ Theorem proving using clausal resolution: from past to present ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ Sublogics of a branching time logic of robustness
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A tableau-based decision procedure for CTL\(^*\)
- The temporal logic of branching time
- Automata-theoretic techniques for modal logics of programs
- A near-optimal method for reasoning about action
- Temporal resolution using a breadth-first search algorithm
- Clausal resolution in a logic of rational agency
- Decision procedures and expressiveness in the temporal logic of branching time
- One-Pass Tableaux for Computation Tree Logic
- A Temporal Logic of Robustness
- A Tableau for RoBCTL
- CTL-RP: A computation tree logic resolution prover
- System Description: Spass Version 3.0
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- “Sometimes” and “not never” revisited
- A clausal resolution method for CTL branching-time temporal logic
- Logic in Computer Science
- Automated Reasoning with Analytic Tableaux and Related Methods
- A Refined Resolution Calculus for CTL
- Tools and Algorithms for the Construction and Analysis of Systems
- Clausal temporal resolution
- Distributed Computing
This page was built for publication: A resolution calculus for the branching-time temporal logic CTL
