 |
    |
InKreSAT: Modal Reasoning via Incremental Reduction to SAT
Mark Kaminski1 and Tobias Tebbi2
1Department of Computer Science, University of Oxford, UK
2Saarland University, Saarbrücken, Germany
Abstract. 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.
LNAI 7898, p. 436 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013