SAT modulo intuitionistic implications

DOI10.1007/978-3-662-48899-7_43MaRDI QIDQ3460091zbMATH OpenOpenAlexFDO

Authors Koen Claessen, Dan Rosen

Publication date 12 January 2016

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-48899-7_43

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• Solving the incremental satisfiability problem
• Ultimately incremental SAT
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
• Optimization techniques for propositional intuitionistic logic and their implementation

Cited in

(14)

• Para-disagreement logics and their implementation through embedding in Coq and SMT
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• An experiment with satisfiability modulo SAT
• General clauses for SAT-based proof search in intuitionistic propositional logic
• intuit
• Efficient SAT-based proof search in intuitionistic propositional logic
• SAT-based proof search in intermediate propositional logics
• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• A tableaux calculus for default intuitionistic logic
• SAT Modulo Differential Equation Simulations
• Non-classical logics in satisfiability modulo theories
• An improved BDD method for intuitionistic propositional logic: BDDIntKt system description
• InKreSAT: modal reasoning via incremental reduction to SAT

This page was built for publication: SAT modulo intuitionistic implications

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