A Refined Resolution Calculus for CTL

DOI10.1007/978-3-642-02959-2_20zbMath1250.03023OpenAlexW1765447656MaRDI QIDQ5191106

Ullrich Hustadt, Clare Dixon, Lan Zhang

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_20

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items

Computing sufficient and necessary conditions in CTL: a forgetting approach, Theorem proving using clausal resolution: from past to present, A resolution calculus for the branching-time temporal logic CTL, First-Order Resolution Methods for Modal Logics, A Refined Resolution Calculus for CTL

Uses Software

• SPASS
• TRP++

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automata-theoretic techniques for modal logics of programs
• Temporal resolution using a breadth-first search algorithm
• Decision procedures and expressiveness in the temporal logic of branching time
• Alternating-time temporal logic
• One-Pass Tableaux for Computation Tree Logic
• System Description: Spass Version 3.0
• 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
• Clausal temporal resolution