InKreSAT: modal reasoning via incremental reduction to SAT. 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.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: (\mathrmK_\mathrmS\mathrmP) a resolution-based theorem prover for (\mathsfK_n): architecture, refinements, strategies and experiments (2020)
- Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
- Lagniez, Jean-Marie; Le Berre, Daniel; de Lima, Tiago; Montmirail, Valentin: An assumption-based approach for solving the Minimal S5-Satisfiability problem (2018)
- Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: (\textK_ \textS\textP): a resolution-based prover for multimodal K (2016)
- Kaminski, Mark; Tebbi, Tobias: InKreSAT: modal reasoning via incremental reduction to SAT (2013)