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

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• A Modular Formalisation of Finite Group Theory
• A goal-directed decision procedure for hybrid PDL
• A new look at generalized rewriting in type theory
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Canonical Big Operators
• Completeness and Decidability Results for CTL in Coq
• Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
• Cut-free sequent systems for temporal logic
• Decision procedures and expressiveness in the temporal logic of branching time
• Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics
• Propositional dynamic logic of regular programs
• Terminating Tableaux for Hybrid Logic with Eventualities
• The Beginning of Model Checking: A Personal Perspective
• The temporal logic of branching time
• Two-Way Automata in Coq
• Using branching time temporal logic to synthesize synchronization skeletons

Cited In (6)

• Constructive completeness for modal logic with transitive closure
• Formalized proof systems for propositional logic
• 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

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)