InKreSAT: modal reasoning via incremental reduction to SAT

DOI10.1007/978-3-642-38574-2_31zbMATH Open1381.68272OpenAlexW139679001MaRDI QIDQ4928458FDOQ4928458

Authors: Mark Kaminski, Tobias Tebbi 

Publication date: 14 June 2013

Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_31

Recommendations

• Modal Satisfiability via SMT Solving
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• scientific article; zbMATH DE number 1765692
• scientific article; zbMATH DE number 1538057
• SAT modulo intuitionistic implications

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Cited In (10)

• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Modal logic S5 satisfiability in answer set programming
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
• InKreSAT
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Local is best: efficient reductions to modal logic \textsf{K}
• Resolution calculi for non-normal modal logics
• Verified Decision Procedures for Modal Logics.
• SAT-based explicit LTL reasoning and its application to satisfiability checking

Uses Software

• MiniSat
• FaCT++
• Spartacus

This page was built for publication: InKreSAT: modal reasoning via incremental reduction to SAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928458)