Verified Decision Procedures for Modal Logics.

DOI10.4230/LIPIcs.ITP.2019.31OpenAlexW2978361984MaRDI QIDQ5875443

Rajeev Goré, Minchao Wu

Publication date: 3 February 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2019/11086/pdf/LIPIcs-ITP-2019-31.pdf/

zbMATH Keywords

modal logicformal methodsinteractive theorem provingLean

Mathematics Subject Classification ID

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

• FaCT++
• Lean
• GitHub
• InKreSAT

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.