A clausal resolution method for branching-time logic ECTL^+

DOI10.1007/S10472-006-9018-1MaRDI QIDQ862827zbMATH OpenOpenAlexFDO

Authors Alexander Bolotov, Artie Basukoski

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

automated deductionbranching-time logicprogram specification and verificationresolution

Mathematics Subject Classification ID

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

Recommendations

• A clausal resolution method for extended computation tree logic ECTL
• A clausal resolution method for CTL branching-time temporal logic
• scientific article; zbMATH DE number 1418334
• A resolution calculus for the branching-time temporal logic CTL
• \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)

Cites work

• A clausal resolution method for CTL branching-time temporal logic
• A clausal resolution method for extended computation tree logic ECTL
• Deciding full branching time logic
• Decision procedures and expressiveness in the temporal logic of branching time
• scientific article; zbMATH DE number 4027441 (Why is no real title available?)
• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• Modal logics and mu-calculi: An introduction
• Resolution theorem proving
• “Sometimes” and “not never” revisited

Cited in

(10)

• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• To be fair, use bundles
• A clausal resolution method for extended computation tree logic ECTL
• One-Pass Tableaux for Computation Tree Logic
• scientific article; zbMATH DE number 1950255 (Why is no real title available?)
• A clausal resolution method for CTL branching-time temporal logic
• scientific article; zbMATH DE number 1418334 (Why is no real title available?)
• A Refined Resolution Calculus for CTL
• A resolution calculus for the branching-time temporal logic CTL
• On the expressive power of the normal form for branching-time temporal logics

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q862827)