CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

SAT modulo intuitionistic implications

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science. Proceedings of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) (0302-9743). Vol. 9450 (2015), p. 622-637.
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2016-01-18. Senast ändrad 2016-07-04.
CPL Pubid: 230822

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Programvaruteknik

Chalmers infrastruktur