SAT modulo intuitionistic implications. We present a new method for solving problems in intuitionistic propositional logic, which involves the use of an incremental SAT-solver. The method scales to very large problems, and fits well into an SMT-based framework for interaction with other theories.
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Ferrari, Mauro; Fiorentini, Camillo: Goal-oriented proof-search in natural deduction for intuitionistic propositional logic (2019)
- Fiorentini, Camillo; Goré, Rajeev; Graham-Lengrand, Stéphane: A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic (2019)
- Woltzenlogel Paleo, Bruno: Para-disagreement logics and their implementation through embedding in Coq and SMT (2018)
- Claessen, Koen; Rosén, Dan: SAT modulo intuitionistic implications (2015)