Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-25T06:00:29.616Z Has data issue: false hasContentIssue false
  • English
  • Français

Modal Logic S5 Satisfiability in Answer Set Programming

Published online by Cambridge University Press:  05 November 2021

MARIO ALVIANO Open the ORCID record for MARIO ALVIANO [Opens in a new window] ,
SOTIRIS BATSAKIS  and
GEORGE BARYANNIS Open the ORCID record for GEORGE BARYANNIS [Opens in a new window]
MARIO ALVIANO
Affiliation:
University of Calabria, Italy (e-mail: [email protected])
SOTIRIS BATSAKIS
Affiliation:
Technical University of Crete, Greece and University of Huddersfield, UK (e-mail: [email protected])
GEORGE BARYANNIS
Affiliation:
School of Computing and Engineering, University of Huddersfield, UK (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

modal logicS5Answer Set ProgrammingKripke semantics
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 21 , Issue 5: 37th International Conference on Logic Programming Special Issue I , September 2021 , pp. 527 - 542
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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.Google Scholar
Auffray, Y. and Hebrard, J.-J. 1990. Strategies for modal resolution: results and problems. Journal of Automated Reasoning 6, 1, 1–38.Google Scholar
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.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Brewka, G., Eiter, T. and Truszczyński, M. 2011. Answer set programming at a glance. Communications of the ACM 54, 12, 92–103.CrossRefGoogle Scholar
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.Google Scholar
Fitting, M. 1999. A simple propositional S5 tableau system. Annals of Pure and Applied Logic 96, 1–3, 107–115.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Goré, R. and Thomson, J. 2019. A correct polynomial translation of s4 into intuitionistic logic. The Journal of Symbolic Logic 84, 2, 439–451.CrossRefGoogle Scholar
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).CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Kripke, S. A. 1959. A completeness theorem in modal logic. The Journal of Symbolic Logic 24, 1, 1–14.Google Scholar
Ladner, R. E. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing 6, 3, 467–480.CrossRefGoogle Scholar
Liau, C.-J. 2003. Belief, information acquisition, and trust in multi-agent systems —a modal logic formulation. Artificial Intelligence 149, 1, 31–60.CrossRefGoogle Scholar
Lifschitz, V. 2019. Answer Set Programming. Springer, Berlin, Heidelberg.CrossRefGoogle Scholar
Moses, Y. 2008. Reasoning about knowledge and belief. Foundations of Artificial Intelligence 3, 621–647.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Nalon, C. and Dixon, C. 2007. Clausal resolution for normal modal logics. Journal of Algorithms 62, 3, 117–134.CrossRefGoogle Scholar
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.Google Scholar
Ohlbach, H. J. 1991. Semantics-based translation methods for modal logics. Journal of Logic and Computation 1, 5, 691–746.CrossRefGoogle Scholar
Plaisted, D. A. and Greenbaum, S. 1986. A structure-preserving clause form translation. Journal of Symbolic Computation 2, 3, 293–304.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar