CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT

DOI10.1007/978-3-030-86059-2_5OpenAlexW3197054820MaRDI QIDQ2142066

Rajeev Goré, Cormac Kikkert

Publication date: 25 May 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-86059-2_5

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• InKreSAT
• BDDTab
• intuit

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