Clausal Tableaux for Multimodal Logics of Belief

• Autorzy: Goré R. , Nguyen L.A. L.A.
• Języki publikacji: EN

Abstrakty

EN

We develop clausal tableau calculi for six multimodal logics variously designed for reasoning about multi-degree belief, reasoning about distributed systems of belief and for reasoning about epistemic states of agents in multi-agent systems. Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, thereby giving decision procedures for all of these logics. We also use our calculi to obtain complexity results for five of these logics. The complexity of the remaining logic was known.

Słowa kluczowe

EN

modal logics for agent-based systems; theorem proving for modal logics; complexity and decidability of modal logics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 94, nr 1
• Strony: 21--40
• Opis fizyczny: Bibliogr. 28 poz.

Twórcy

autor

Goré R.

autor

Nguyen L.A. L.A.

• Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland.,

Bibliografia

• [1] Aldewereld, H., van der Hoek, W., Meyer, J.-J.: Rational Teams: Logical Aspects of Multi-Agent Systems, Fundamenta Informaticae, 63(2-3), 2004, 159-183.
• [2] Baldoni, M., Giordano, L., Martelli, A.: A Tableau Calculus for Multimodal Logics and some (Un)Decidability Results, H. de Swart, editor, Proceeding of TABLEAUX'98, LNCS 1397, Springer-Verlag, 1998.
• [3] del Cerro, L. F., Penttonent, M.: Grammar Logics, Logique et Analyse, 121-122, 1988, 123-134.
• [4] Debart, F., Enjalbert, P., Lescot, M.: Multimodal Logic Programming Using Equational and Order-Sorted Logic, Theoretical Comp. Science, 105, 1992, 141-166.
• [5] Demri, S.: The Complexity of Regularity in Grammar Logics and Related Modal Logics., Journal of Logic and Computation, 11(6), 2001, 933-960.
• [6] Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge, MIT Press, 1995.
• [7] Fitting, M.: Proof Methods for Modal and Intuitionistic Logics, Volume 169 of Synthese Library. D. Reidel, Dordrecht, Holland, 1983.
• [8] Fitting, M., Thalmann, L., Voronkov, A.: Term-Modal Logics, Studia Logica, 69, 2001, 133-169.
• [9] Gorè, R.: TableauMethods forModal and Temporal Logics, in: Handbook of Tableau Methods (D'Agostino, Gabbay, Hähnle, Posegga, Eds.), Kluwer Academic Publishers, 1999, 297-396.
• [10] Gorè, R., Nguyen, L. A.: Analytic Cut-free Tableaux for Regular Modal Logics of Agent Beliefs, Proceedings of CLIMA VIII, LNAI 5056 (F. Sadri, K. Satoh, Eds.), Springer-Verlag, 2008.
• [11] Governatori, G.: Labelled Tableaux for Multi-Modal Logics, Proceedings of TABLEAUX'1995, LNAI 918 (P. Baumgartner, R. Hähnle, J. Posegga, Eds.), Springer-Verlag, 1995.
• [12] Halpern, J., Moses, Y.: A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief, Artificial Intelligence, 54, 1992, 319-379.
• [13] Hintikka, K.: Form and content in quantification theory, Acta Philosophica Fennica, 8, 1955, 3-55.
• [14] Hudelmaier, J.: Improved Decision Procedures for the Modal Logics K, T, S4, H.K. Büning, editor, Proc. Of CSL'95, LNCS 1092, Springer, 1996.
• [15] Massacci, F.: Single Step Tableaux for Modal Logics, Journal of Automated Reasoning, 24(3), 2000, 319-364.
• [16] Meyer, J.-J., de Boer, F., van Eijk, R., Hindriks, K., van der Hoek, W.: On Programming KARO Agents, Logic Journal of the IGPL, 9(2), 2001.
• [17] Meyer, J.-J., van der Hoek, W.: A modal logic for nonmonotonic reasoning, chapter 3, Ellis Horwood, 1992, 37-79.
• [18] Meyer, J.-J., van der Hoek,W.: Epistemic Logic for Computer Science and Artificial Intelligence, Cambridge University Press, 1995.
• [19] Mints, G.: Gentzen-type Systems and Resolution Rules, P.Martin-Lőf, G. Mints (eds.): COLOG-88, LNCS 417, Springer, 1988.
• [20] Nguyen, L.: A New Space Bound for the Modal Logics K4, KD4 and S4, Proceedings of MFCS'99, LNCS 1672 (M. Kutylowski, L. Pacholski, Eds.), Springer, 1999.
• [21] Nguyen, L.: Clausal Tableau Systems and Space Bounds for the Modal Logics K, KD, T, KB, KDB, and B, Technical Report TR 00-01(261), Institute of Informatics, University of Warsaw, 2000.
• [22] Nguyen, L.: Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD5, Studia Logica, 69(1), 2001, 41-57.
• [23] Nguyen, L.: Multimodal Logic Programming, Theoretical Computer Science, 360, 2006, 247-288.
• [24] Nguyen, L.: Foundations of Modal Deductive Databases, Fundamenta Informaticae, 79(1-2), 2007, 85-135.
• [25] Rautenberg,W.: Modal tableau calculi and interpolation, Journal of Philosophical Logic, 12, 1983, 403-423.
• [26] Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, Pearson Education, 2003.
• [27] Schmidt, R., Tishkovsky, D., Hustadt, U.: Interactions between Knowledge, Action, and Commitment within Agent Dynamic Logic, Studia Logica, 78(3), 2004, 381-415.
• [28] Wooldridge, M., Dixon, C., Fisher, M.: A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief, Journal of Applied Non-Classical Logics, 8(3), 1998, 225-258.