Verified Decision Procedures for Modal Logics.
From MaRDI portal
Publication:5875443
DOI10.4230/LIPIcs.ITP.2019.31OpenAlexW2978361984MaRDI QIDQ5875443
Publication date: 3 February 2023
Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2019/11086/pdf/LIPIcs-ITP-2019-31.pdf/
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Formalized soundness and completeness of epistemic logic ⋮ A henkin-style completeness proof for the modal logic S5 ⋮ Verification of dynamic bisimulation theorems in Coq
Uses Software
Cites Work
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of the resolution calculus for first-order logic
- Verifying the LTL to Büchi automata translation via very weak alternating automata
- A benchmark method for the propositional modal logics K, KT, S4
- Formally verified tableau-based reasoners for a description logic
- The algebra of topology
- Logic and Categories As Tools For Building Theories
- Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
- Implementing Tableau Calculi Using BDDs: BDDTab System Description
- The Lean Theorem Prover (System Description)
- A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic
- Efficient loop-check for backward proof search in some non-classical propositional logics
- InKreSAT: Modal Reasoning via Incremental Reduction to SAT
- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
- Some theorems about the sentential calculi of Lewis and Heyting
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Verified Decision Procedures for Modal Logics.
