Completeness and Decidability Results for CTL in Coq
From MaRDI portal
Publication:2879254
DOI10.1007/978-3-319-08970-6_15zbMath1416.68159OpenAlexW2142533042MaRDI QIDQ2879254
Gert Smolka, Christian Doczkal
Publication date: 8 September 2014
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-08970-6_15
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)
Related Items (3)
Completeness and decidability results for CTL in constructive type theory ⋮ Certifying standard and stratified Datalog inference engines in SSReflect ⋮ A henkin-style completeness proof for the modal logic S5
Uses Software
This page was built for publication: Completeness and Decidability Results for CTL in Coq
