A clausal resolution method for branching-time logic \(\text{ECTL}^+\)

DOI10.1007/s10472-006-9018-1zbMath1112.03010OpenAlexW1983538726MaRDI QIDQ862827

Artie Basukoski, Alexander Bolotov

Publication date: 24 January 2007

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-006-9018-1

zbMATH Keywords

resolutionautomated deductionbranching-time logicprogram specification and verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

To be fair, use bundles ⋮ One-Pass Tableaux for Computation Tree Logic

Cites Work

• Decision procedures and expressiveness in the temporal logic of branching time
• A clausal resolution method for extended computation tree logic ECTL
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• A clausal resolution method for CTL branching-time temporal logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A clausal resolution method for branching-time logic \(\text{ECTL}^+\)