CTL-RP: A computation tree logic resolution prover

DOI10.3233/AIC-2010-0463MaRDI QIDQ3568224zbMATH OpenOpenAlexFDO

Authors Lan Zhang, Ullrich Hustadt, Clare Dixon

Publication date 17 June 2010

Published in AI Communications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/aic-2010-0463

zbMATH Keywords

branching-time temporal logics, resolution theorem proving

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Recommendations

• A Refined Resolution Calculus for CTL
• A resolution calculus for the branching-time temporal logic CTL
• A clausal resolution method for CTL branching-time temporal logic
• A tableau-based decision procedure for CTL^*
• A clausal resolution method for extended computation tree logic ECTL

Cited in

(6)

• Theorem proving using clausal resolution: from past to present
• CTL-RP
• First-order resolution methods for modal logics
• 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

Describes a project that uses

Uses Software

• TRP++
• SPASS

This page was built for publication: CTL-RP: A computation tree logic resolution prover

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