Skip to main content

MoSaiC

A RECAR Approach For Solving Modal Logics Satisfiability Problems

Linux View source Mac OS X

Benchmarks used

Modal Logic K

Modal Logic KT

Modal Logic S4

Modal Logic K

3CNF-KSP (3.4MB, 30MB decompressed) [1]
qbf (860kB, 46MB decompressed) [2]
qbfL (530kB, 17MB decompressed) [2]
qbfS (108kB, 2.2MB decompressed) [2]
qbfMS (176kB, 7.0MB decompressed) [2]
qbfML (1.7MB, 187MB decompressed0) [2]
LWB_K (bash scripts, 260kB, rougly 14 GB) [3]

Modal Logic KT

LWB_KT (bash scripts, 260kB, rougly 18 GB) [3]

Modal Logic S4

LWB_S4 (bash scripts, 260kB, rougly 13 GB) [3]

State-of-the-art Solvers

Modal Logic K

Modal Logic KT

Modal Logic S4

Experimental Results

Modal Logic K

3CNF-KSP [1]

Cactus-3CNF-K

MQBF (qbf + qbfS + qbfL + qbfMS + qbfML) [2]

Cactus-MQBF-K

LWB_K [3]

Cactus-LWB-K

3CNF-KSP + MQBF + LWB_K

Cactus-All-K

Modal Logic KT

LWB_KT [3]

Cactus-LWB-KT

Modal Logic S4

LWB_S4 [3]

Cactus-LWB-S4

Scatter-Plot of MoSaiC againt something

Scatter

Bibliography

Articles about benchmarks

[1] : Patel-Schneider, P.F., Sebastiani, R.: A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. JAIR 18 (2003) 351–389

[2] :
- Massacci, F., Donini, F.M.: Design and results of TANCS-2000 non-classical (modal) systems comparison. In: Proc. of TABLEAUX’00. (2000) 52–56
- + Kaminski, M., Tebbi, T.: InKreSAT: Modal Reasoning via Incremental Reduction to SAT. In: Proc. of CADE’13. (2013) 436–442

[3] : Balsiger, P., Heuerding, A., Schwendimann, S.: A Benchmark Method for the Propositional Modal Logics K, KT, S4. J. Autom. Reasoning 24(3) (2000) 297–317

Articles about solvers

[4]: Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-Based Decision Procedures for Classical Modal Logics. J. Autom. Reasoning 28(2) (2002) 143–171

[5]: Goré, R., Olesen, K., Thomson, J.: Implementing Tableau Calculi Using BDDs: BDDTab System Description. In: Proc. of IJCAR’14. (2014) 337–343

[6]: Tsarkov, D., Horrocks, I.: FaCT++ Description Logic Reasoner: System Description. In: Proc. of IJCAR’06. (2006) 292–297

[7]: Kaminski, M., Tebbi, T.: InKreSAT: Modal Reasoning via Incremental Reduction to SAT. In: Proc. of CADE’13. (2013) 436–442

[8]: Sebastiani,R.,Vescovi,M.: Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. JAIR 35 (2009) 343–389

[9]: Nalon, C., Hustadt, U., Dixon, C.: K_SP : A Resolution-Based Prover for Multimodal K. In: Proc. of IJCAR’16. (2016) 406–415

[10]: Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: A Tableau Prover for Hybrid Logic. Electr. Notes Theor. Comput. Sci. 262 (2010) 127–139

[11]: Kovàcs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: Proc. of CAV’13. (2013) 1–35