InKreSAT: modal reasoning via incremental reduction to SAT

DOI10.1007/978-3-642-38574-2_31MaRDI QIDQ4928458zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(10)

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

Describes a project that uses

Uses Software

• Spartacus
• FaCT++
• MiniSat

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)