And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
From MaRDI portal
Publication:3192179
DOI10.1007/978-3-319-08587-6_3zbMath1423.68415OpenAlexW87797281MaRDI QIDQ3192179
Publication date: 26 September 2014
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1885/74602
Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)
Related Items (6)
Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ The Proof Theory of Common Knowledge ⋮ Verified Decision Procedures for Modal Logics. ⋮ One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
This page was built for publication: And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
