Completeness and decidability results for CTL in constructive type theory
From MaRDI portal
Publication:287375
DOI10.1007/s10817-016-9361-9zbMath1356.03053OpenAlexW2293203053MaRDI QIDQ287375
Christian Doczkal, Gert Smolka
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9361-9
completenessdecidabilityinteractive theorem provingCoqcomputation tree logic (CTL)constructive proofsHilbert axiomatizationsSsreflect
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The temporal logic of branching time
- Cut-free sequent systems for temporal logic
- Using branching time temporal logic to synthesize synchronization skeletons
- Propositional dynamic logic of regular programs
- Decision procedures and expressiveness in the temporal logic of branching time
- A goal-directed decision procedure for hybrid PDL
- Two-Way Automata in Coq
- Infinite sets that Satisfy the Principle of Omniscience in any Variety of Constructive Mathematics
- Completeness and Decidability Results for CTL in Coq
- A Constructive Proof of Dependent Choice, Compatible with Classical Logic
- Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
- The Beginning of Model Checking: A Personal Perspective
- A Modular Formalisation of Finite Group Theory
- Canonical Big Operators
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Terminating Tableaux for Hybrid Logic with Eventualities
This page was built for publication: Completeness and decidability results for CTL in constructive type theory
