Completeness and decidability results for CTL in constructive type theory

DOI10.1007/S10817-016-9361-9MaRDI QIDQ287375zbMATHOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• 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)

• Mechanising Gödel-Löb provability logic in HOL light
• Completeness and Decidability Results for CTL in Coq
• Constructive completeness for modal logic with transitive closure
• Constructive and mechanised meta-theory of intuitionistic epistemic logic
• Completeness in hybrid type theory
• Formalized proof systems for propositional logic

Describes a project that uses

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)