Verified Decision Procedures for Modal Logics.
From MaRDI portal
Cites work
- A benchmark method for the propositional modal logics K, KT, S4
- A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic
- A verified SAT solver framework with learn, forget, restart, and incrementality
- And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
- Efficient loop-check for backward proof search in some non-classical propositional logics
- Formalization of the resolution calculus for first-order logic
- Formally verified tableau-based reasoners for a description logic
- scientific article; zbMATH DE number 1936671 (Why is no real title available?)
- scientific article; zbMATH DE number 824735 (Why is no real title available?)
- Implementing tableau calculi using BDDs: BDDTab system description
- InKreSAT: modal reasoning via incremental reduction to SAT
- Logic and categories as tools for building theories
- MLAT: a tool for heap analysis based on predicate abstraction by modal logic
- Optimal and cut-free tableaux for propositional dynamic logic with converse
- Some theorems about the sentential calculi of Lewis and Heyting
- Tableau methods for modal and temporal logics
- The algebra of topology
- The Lean theorem prover (system description)
- Verifying the LTL to Büchi automata translation via very weak alternating automata
Cited in
(12)- SAT-based decision procedures for classical modal logics
- Verification of dynamic bisimulation theorems in Coq
- Formalized soundness and completeness of epistemic logic
- A henkin-style completeness proof for the modal logic S5
- Modal logics for cryptographic processes
- BDD-based decision procedures for the modal logic K ★
- scientific article; zbMATH DE number 3918335 (Why is no real title available?)
- Decision procedures for BDI logics
- Improved decision procedures for multi-modal tense logic using CEGAR-tableaux
- Formalized soundness and completeness of epistemic and public announcement logic
- Model construction for modal clauses
- Verified tableaux: from modal logics to modal fixpoint logics
This page was built for publication: Verified Decision Procedures for Modal Logics.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875443)
