×

zbMATH — the first resource for mathematics

SAT modulo intuitionistic implications. (English) Zbl 1435.68363
Davis, Martin (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 20th international conference, LPAR-20 2015, Suva, Fiji, November 24–28, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9450, 622-637 (2015).
Summary: 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.
For the entire collection see [Zbl 1326.68013].

MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B20 Subsystems of classical logic (including intuitionistic logic)
Software:
intuit
PDF BibTeX XML Cite
Full Text: DOI