SAT modulo intuitionistic implications
Paper i proceeding, 2015
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.
Författare
Koen Lindström Claessen
Chalmers, Data- och informationsteknik, Programvaruteknik
Dan Rosén
Chalmers, Data- och informationsteknik, Programvaruteknik
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
03029743 (ISSN) 16113349 (eISSN)
Vol. 9450 622-637978-3-662-48898-0 (ISBN)
Ämneskategorier
Programvaruteknik
DOI
10.1007/978-3-662-48899-7_43
ISBN
978-3-662-48898-0