A Fixpoint Semantics and an SLD-Resolution Calculus for Modal Logic Programs

• Autorzy: Nguyen L.A.
• Języki publikacji: EN

Abstrakty

EN

We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, S4, KD5, KD45, and S5. For an MProlog program P and for L being one of the mentioned logics, we define an operator T_L,P, which has the least fixpoint I_L,P. This fixpoint is a set of formulae, which may contain labeled forms of the modal operator , and is called the leasta-model generator of P. The standard model of I_L,P is shown to be a least L-model of P. The SLD-resolution calculus for MProlog is designed with a similar style as for classical logic programming. It is sound and complete. We also extend the calculus for MProlog in the almost serial modal logics KB, K5, K45, and KB5.

Słowa kluczowe

EN

modal logic programs; Kripke models; MProlog language; model generator

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 1
• Strony: 63--100
• Opis fizyczny: bibliogr. 34 poz.

Twórcy

autor

Nguyen L.A.

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

Bibliografia

• [1] Abadi, M., Manna, Z.: Temporal Logic Programming, Journal of Symbolic Computation, 8, 1989, 277-295.
• [2] Akama, S.: A Meta-Logical Foundation of Modal Logic Programming. 1-20-1, Higashi-Yurigaoka, Asao-ku, Kawasaki-shi, 215, Japan, December 1989.
• [3] Aoyagi, T., Fujita, M., Moto-oka, T.: Temporal Logic Programming Language Tokio, E. Wada, editor, Logic Programming’85, LNCS 221, Springer-Verlag, 1986.
• [4] Apt, K.: Logic Programming, in: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (J. van Leeuwen, Ed.), Elsevier, 1990.
• [5] Balbiani, P., Fari˜nas del Cerro, L., Herzig, A.: Declarative Semantics for Modal Logic Programs, Proceedings of the 1988 International Conference on Fifth Generation Computer Systems, ICOT, 1988.
• [6] Balbiani, P., Herzig, A., Lima-Marques, M.: TIM: The Toulouse Inference Machine for Non-Classical Logic Programming, PDK’91: International Workshop on Processing Declarative Knowledge, Springer-Verlag, 1991.
• [7] Balbiani, P., Herzig, A., Lima-Marques, M.: Implementing Prolog Extensions: A Parallel Inference Machine, Proceedings of the 1992 International Conference on Fifth Generation Computer Systems, ICOT, 1992.
• [8] Barringer, H., Fisher, M., Gabbay, D., Gough, G., Owens, R.: METATEM: A Framework for Programming in Temporal Logic, Proceedings of REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, LNCS 430, Springer-Verlag, 1989.
• [9] Brzoska, C.: Temporal Logic Programming with Metric and Past Operators, Executable Modal and Temporal Logics, IJCAI’93 workshop, M. Fisher and R. Owens (eds.), Springer, 1995.
• [10] Farinas del Cerro, L.: MOLOG: A System that Extends PROLOG with Modal Logic, New Generation Computing, 4, 1986, 35-50.
• [11] Farinas del Cerro, L., Penttonen, M.: A Note on the Complexity of the Satisfiability of Modal Horn Clauses, Logic Programming, 4, 1987, 1-10.
• [12] Chen, C., Lin, I.: The Computational Complexity of the Satisfiability of Modal Horn Clauses for Modal Propositional Logics, Theoretical Computer Science, 129, 1994, 95-121.
• [13] Debart, F., Enjalbert, P., Lescot, M.: Multimodal Logic Programming Using Equational and Order-Sorted Logic, Theoretical Computer Science, 105, 1992, 141-166.
• [14] Fisher, M., Owens, R.: From the Past to the Future: Executing Temporal Logic Programs, Proceedings of Logic Programming and Automated Reasoning, LNCS 624, Springer-Verlag, 1992.
• [15] Fisher, M., Owens, R.: An Introduction to Executable Modal and Temporal Logics, Executable Modal and Temporal Logics, IJCAI’93 workshop, M. Fisher and R. Owens (eds.), Springer, 1995.
• [16] Gabbay, D.: Modal and Temporal Logic II (A Temporal Logic Machine), in: Logic Programming–Expanding the Horizon (T. Dodd, R. Owens, S. Torrance, Eds.), Intellect Books Ltd, 1991.
• [17] Garson, J.: Quantification in Modal Logic, in: Handbook of Philosophical Logic, Volume II (F. Guenthner, D. Gabbay, Eds.), 1999, 249-307.
• [18] Hale, R.: Temporal Logic Programming, in: Temporal Logics and Their Applications (A. Galton, Ed.), Academic Press, 1987, 91-119.
• [19] Halpern, J.: The Effect of Bounding the Number of Primitive Propositions and the Depth of Nesting on the Complexity of Modal Logic, Artificial Intelligence, 75, 1995.
• [20] Hrycej, T.: Temporal Prolog, Yves Kodratoff, editor, Proceedings of the European Conference on Artificial Intelligence, Pitman Publishing, 1988.
• [21] Hrycej, T.: A Temporal Extension of Prolog, The Journal of Logic Programming, 15(1&2), 1993, 113-145.
• [22] Hudelmaier, J.: Improved Decision Procedures for the Modal Logics K, T, S4, H. Kleine Büning, editor, Proceedings of CSL’95, LNCS 1092, Springer, 1996.
• [23] Leitsch, A.: The Resolution Calculus, Springer, 1997.
• [24] Lloyd, J.: Foundations of Logic Programming, Second Edition, Springer-Verlag, 1987.
• [25] Minker, J.: Logic and Databases: A 20-Year Retrospective, International Workshop LID’96, Verlag pringer, 1996.
• [26] Mints, G.: Gentzen-type Systems and Resolution Rules, P.Martin-L¨of, G. Mints (eds.): COLOG-88, LNCS 417, Springer, 1988.
• [27] Moszkowski, B.: Executing Temporal Logic Programs, Cambridge University Press, 1986.
• [28] Nguyen, L.: A Fixpoint Semantics and an SLD-Resolution Calculus for Modal Logic Programs, Technical Report TR 01-02 (265), Institute of Informatics, Warsaw University, 2001 (last revised January, 2003). Available on http://www.mimuw.edu.pl/˜nguyen/papers.html.
• [29] Nguyen, L.: Constructing the Least Models for Positive Modal Logic Programs, Fundamenta Informaticae, 42(1), 2000, 29-60.
• [30] Nguyen, L.: The Modal Query Language MDatalog, Fundamenta Informaticae, 46(2001), 2001, 315-342.
• [31] Ohlbach, H.: A Resolution Calculus for Modal Logics, Proceedings of CADE-88, LNCS310, Springer, 1988.
• [32] Orgun, M., Ma, W.: An Overview of Temporal and Modal Logic Programming, D.M. Gabbay and H.J. Ohlbach, editors, Proc. First Int. Conf. on Temporal Logic - LNAI 827, Springer-Verlag, 1994.
• [33] Orgun, M., Wadge, W.: Chronolog: A Temporal Logic Programming Language and Its Formal Semantics, Department of Computer Science, University of Victoria, Victoria, B.C., Canada, 1988.
• [34] Rolston, D.: Chronolog: A Pure Tense-Logic-Based Infinite-Object Programming Language, Department of Computer Science and Engineering, Arizona State University, Tempe, Arizona, 1986.