CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
From MaRDI portal
Publication:2142066
DOI10.1007/978-3-030-86059-2_5OpenAlexW3197054820MaRDI QIDQ2142066
Publication date: 25 May 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-86059-2_5
Related Items (4)
Mechanising Gödel-Löb provability logic in HOL light ⋮ Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic ⋮ SAT-based proof search in intermediate propositional logics ⋮ Local reductions for the modal cube
Uses Software
Cites Work
- Unnamed Item
- A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- Implementing Tableau Calculi Using BDDs: BDDTab System Description
- Clausal Tableaux for Multimodal Logics of Belief
- SAT Modulo Intuitionistic Implications
- The Taming of the Cut. Classical Refutations with Analytic Cut
- InKreSAT: Modal Reasoning via Incremental Reduction to SAT
- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
This page was built for publication: CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT