Modal logic S5 satisfiability in answer set programming. (English) Zbl 07454767

Summary: Modal logic S5 has attracted significant attention and has led to several practical applications, owing to its simplified approach to dealing with nesting modal operators. Efficient implementations for evaluating satisfiability of S5 formulas commonly rely on Skolemisation to convert them into propositional logic formulas, essentially by introducing copies of propositional atoms for each set of interpretations (possible worlds). This approach is simple, but often results into large formulas that are too difficult to process, and therefore more parsimonious constructions are required. In this work, we propose to use Answer Set Programming for implementing such constructions, and in particular for identifying the propositional atoms that are relevant in every world by means of a reachability relation. The proposed encodings are designed to take advantage of other properties such as entailment relations of subformulas rooted by modal operators. An empirical assessment of the proposed encodings shows that the reachability relation is very effective and leads to comparable performance to a state-of-the-art S5 solver based on SAT, while entailment relations are possibly too expensive to reason about and may result in overhead.


68N17 Logic programming
Full Text: DOI arXiv


[1] Abate, P., Goré, R. and Widmann, F.2007. Cut-free single-pass tableaux for the logic of common knowledge. In Workshop on Agents and Deduction at TABLEAUX. · Zbl 1137.03304
[2] Auffray, Y. and Hebrard, J.-J.1990. Strategies for modal resolution: results and problems. Journal of Automated Reasoning 6, 1, 1-38. · Zbl 0709.03008
[3] Baryannis, G., Tachmazidis, I., Batsakis, S., Antoniou, G., Alviano, M. and Papadakis, E.2020. A generalised approach for encoding and reasoning with qualitative theories in answer set programming. Theory and Practice of Logic Programming 20, 5, 687-702. · Zbl 1468.68218
[4] Baryannis, G., Tachmazidis, I., Batsakis, S., Antoniou, G., Alviano, M., Sellis, T. and Tsai, P.-W.2018. A trajectory calculus for qualitative spatial reasoning using answer set programming. Theory and Practice of Logic Programming 18, 3-4, 355-371. · Zbl 1451.68252
[5] Batsakis, S., Baryannis, G., Governatori, G., Tachmazidis, I. and Antoniou, G.2018. Legal representation and reasoning in practice: A critical comparison. In Legal Knowledge and Information Systems - JURIX 2018: The Thirty-first Annual Conference. IOS Press, Netherlands, 31-40.
[6] Brewka, G., Eiter, T. and Truszczyński, M.2011. Answer set programming at a glance. Communications of the ACM 54, 12, 92-103.
[7] Caridroit, T., Lagniez, J.-M., Berre, D. L., De Lima, T. and Montmirail, V.2017. A sat-based approach for solving the modal logic s5-satisfiability problem. In Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, AAAI 2017. AAAI Press, Palo Alto, California, 3864-3870.
[8] Fitting, M.1999. A simple propositional S5 tableau system. Annals of Pure and Applied Logic 96, 1-3, 107-115. · Zbl 0972.03017
[9] Gasquet, O., Herzig, A., Longin, D. and Sahade, M.2005. LoTREC: Logical Tableaux Research Engineering Companion. In Automated Reasoning with Analytic Tableaux and Related Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, 318-322. · Zbl 1142.68497
[10] Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T. and Wanko, P.2016. Theory solving made easy with clingo 5. In Technical Communications of the Thirty-second International Conference on Logic Programming (ICLP 2016), M. Carro and A. King, Eds. Open Access Series in Informatics (OASIcs), vol. 52. Schloss Dagstuhl, Dagstuhl, Germany, 2:1-2:15.
[11] Giunchiglia, E., Sebastiani, R., Giunchiglia, F. and Tacchella, A.2000. Sat vs. translation based decision procedures for modal logics: a comparative evaluation. Journal of Applied Non-Classical Logics 10, 2, 145-172. · Zbl 1033.03500
[12] Goré, R.1999. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, M. D’Agostino, D. M. Gabbay, R. Hähnle and J. Posegga, Eds. Springer, Netherlands, 297-396. · Zbl 0972.03529
[13] Goré, R. and Thomson, J.2019. A correct polynomial translation of s4 into intuitionistic logic. The Journal of Symbolic Logic 84, 2, 439-451. · Zbl 1457.03041
[14] Götzmann, D., Kaminski, M. and Smolka, G.2010. Spartacus: A tableau prover for hybrid logic. Electronic Notes in Theoretical Computer Science 262, 127-139. Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009).
[15] Hella, L., Järvisalo, M., Kuusisto, A., Laurinharju, J., Lempiäinen, T., Luosto, K., Suomela, J. and Virtema, J.2015. Weak Models of Distributed Computing, with Connections to Modal Logic. Distributed Computing 28, 1, 31-53. · Zbl 1322.68075
[16] Huang, P., Liu, M., Wang, P., Zhang, W., Ma, F. and Zhang, J.2019. Solving the satisfiability problem of modal logic S5 guided by graph coloring. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, S. Kraus, Ed. ijcai.org, California, 1093-1100.
[17] Kaminski, M. and Tebbi, T.2013. Inkresat: Modal reasoning via incremental reduction to sat. In International Conference on Automated Deduction. Springer, Berlin, Heidelberg, 436-442. · Zbl 1381.68272
[18] Kripke, S. A.1959. A completeness theorem in modal logic. The Journal of Symbolic Logic 24, 1, 1-14. · Zbl 0091.00902
[19] Ladner, R. E.1977. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing 6, 3, 467-480. · Zbl 0373.02025
[20] Liau, C.-J.2003. Belief, information acquisition, and trust in multi-agent systems —a modal logic formulation. Artificial Intelligence 149, 1, 31-60. · Zbl 1082.68822
[21] Lifschitz, V.2019. Answer Set Programming. Springer, Berlin, Heidelberg. · Zbl 1480.68003
[22] Moses, Y.2008. Reasoning about knowledge and belief. Foundations of Artificial Intelligence 3, 621-647.
[23] Moss, L. S. and Tiede, H.-J.2007. 19 applications of modal logic in linguistics. In Handbook of Modal Logic, P. Blackburn, J. Van Benthem, and F. Wolter, Eds. Studies in Logic and Practical Reasoning, vol. 3. Elsevier, Amsterdam, 1031-1076.
[24] Nalon, C. and Dixon, C.2007. Clausal resolution for normal modal logics. Journal of Algorithms 62, 3, 117-134. · Zbl 1131.03007
[25] Nalon, C., Hustadt, U., and Dixon, C.2017. Ksp: A resolution-based prover for multimodal K, abridged report. In IJCAI. Vol. 17. ijcai.org, California, 4919-4923.
[26] Ohlbach, H. J.1991. Semantics-based translation methods for modal logics. Journal of Logic and Computation 1, 5, 691-746. · Zbl 0746.03010
[27] Plaisted, D. A. and Greenbaum, S.1986. A structure-preserving clause form translation. Journal of Symbolic Computation 2, 3, 293-304. · Zbl 0636.68119
[28] Pnueli, A.1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). IEEE Computer Society, Los Alamitos, CA, USA, 46-57.
[29] Sebastiani, R. and Vescovi, M.2009. Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. Journal of Artificial Intelligence Research 35, 343-389. · Zbl 1180.68257
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.