Completeness and decidability results for CTL in constructive type theory

DOI10.1007/S10817-016-9361-9zbMATH Open1356.03053OpenAlexW2293203053MaRDI QIDQ287375FDOQ287375

Authors: 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

Recommendations

• Completeness and Decidability Results for CTL in Coq
• Constructive completeness for modal logic with transitive closure
• Decision procedures and expressiveness in the temporal logic of branching time
• An axiomatization of full computation tree logic
• The temporal logic of branching time

zbMATH Keywords

completenessdecidabilitycomputation tree logic (CTL)constructive proofsCoqHilbert axiomatizationsinteractive theorem provingSsreflect

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Categoricity and completeness of theories (03C35)

Cites Work

• Propositional dynamic logic of regular programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Using branching time temporal logic to synthesize synchronization skeletons
• 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
• A new look at generalized rewriting in type theory
• The Beginning of Model Checking: A Personal Perspective
• A Modular Formalisation of Finite Group Theory
• Canonical Big Operators
• Title not available (Why is that?)
• Terminating Tableaux for Hybrid Logic with Eventualities
• The temporal logic of branching time
• Cut-free sequent systems for temporal logic

Cited In (5)

• Constructive and mechanised meta-theory of intuitionistic epistemic logic
• Completeness in hybrid type theory
• Mechanising Gödel-Löb provability logic in HOL light
• Completeness and Decidability Results for CTL in Coq
• Title not available (Why is that?)

Uses Software

• Coq
• CTL
• Coq/SSReflect

This page was built for publication: Completeness and decidability results for CTL in constructive type theory

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