Publication details

Saarland University Computer Science

InKreSAT: Modal Reasoning via Incremental Reduction to SAT

Mark Kaminski, Tobias Tebbi

CADE-24, Vol. 7898 of LNCS, pp. 436-442, Springer, June 2013

InKreSAT is a prover for the modal logics K, T, K4, and S4. InKreSAT reduces a given modal satisfiability problem to a Boolean satisfiability problem, which is then solved using a SAT solver. InKreSAT improves on previous work by proceeding incrementally. It interleaves translation steps with calls to the SAT solver and uses the feedback provided by the SAT solver to guide the translation. This results in better performance and allows to integrate blocking mechanisms known from modal tableau provers. Blocking, in turn, further improves performance and makes the approach applicable to the logics K4 and S4.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy