A clausal resolution method for CTL branching-time temporal logic

DOI10.1080/095281399146625zbMath1054.68666OpenAlexW1969550103WikidataQ98284053 ScholiaQ98284053MaRDI QIDQ4421285

Alexander Bolotov

Publication date: 1999

Published in: Journal of Experimental & Theoretical Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/095281399146625

zbMATH Keywords

Computation Tree Logic

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (10)

A clausal resolution method for branching-time logic \(\text{ECTL}^+\) ⋮ Invariant-free clausal temporal resolution ⋮ Theorem proving using clausal resolution: from past to present ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING ⋮ Alternating automata and temporal logic normal forms ⋮ A clausal resolution method for extended computation tree logic ECTL ⋮ A Refined Resolution Calculus for CTL ⋮ Clausal resolution in a logic of rational agency

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modalities for model checking: Branching time logic strikes back
• Decision procedures and expressiveness in the temporal logic of branching time
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution

This page was built for publication: A clausal resolution method for CTL branching-time temporal logic