An SLD-Resolution Calculus for Basic Serial Multimodal Logics

  • Linh Anh Nguyen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


We develop semantics for modal logic programs in basic serial multimodal logics, which are parameterized by an arbitrary combination of generalized versions of axioms T, B, 4, 5 (in the form, e.g., 4:□ i ϕ→□ j k ϕ) and I:□ i ϕ→□ j ϕ. We do not assume any special restriction for the form of programs and goals. Our fixpoint semantics and SLD-resolution calculus are defined using the direct approach and closely reflect the axioms of the used modal logic. We prove that our SLD-resolution calculus is sound and complete.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Balbiani, P., Fariñas del Cerro, L., Herzig, A.: Declarative semantics for modal logic programs. In: Proceedings of the 1988 International Conference on Fifth Generation Computer Systems, pp. 507–514. ICOT (1988)Google Scholar
  2. 2.
    Baldoni, M., Giordano, L., Martelli, A.: A framework for a modal logic programming. In: Joint International Conference and Symposium on Logic Programming, pp. 52–66. MIT Press, Cambridge (1996)Google Scholar
  3. 3.
    Cresswell, M.J., Hughes, G.E.: A New Introduction to Modal Logic. Routledge, New York (1996)zbMATHGoogle Scholar
  4. 4.
    Debart, F., Enjalbert, P., Lescot, M.: Multimodal logic programming using equational and order-sorted logic. Theoretical Comp. Science 105, 141–166 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Demri, S.: The complexity of regularity in grammar logics and related modal logics. Journal of Logic and Computation 11(6), 933–960 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Fariñas del Cerro, L.: Molog: A system that extends Prolog with modal logic. New Generation Computing 4, 35–50 (1986)zbMATHCrossRefGoogle Scholar
  7. 7.
    Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  8. 8.
    Kowalski, R.A.: Predicate logic as a programming language. In: Rosenfeld, J.L. (ed.) Information Processing of IFIP Congress 74, pp. 569–574 (1974)Google Scholar
  9. 9.
    Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)zbMATHGoogle Scholar
  10. 10.
    Nguyen, L.A.: A fixpoint semantics and an SLD-resolution calculus for modal logic programs. Fundamenta Informaticae 55(1), 63–100 (2003)zbMATHMathSciNetGoogle Scholar
  11. 11.
    Nguyen, L.A.: Multimodal logic programming and its applications to modal deductive databases. Manuscript (served as a technical report), available on Internet at (2003),
  12. 12.
    Nguyen, L.A.: The modal logic programming system MProlog. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 266–278. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Nguyen, L.A.: The modal logic programming system MProlog: Theory, design, and implementation (2005), Available at
  14. 14.
    Nonnengart, A.: How to use modalities and sorts in Prolog. In: MacNish, C., Moniz Pereira, L., Pearce, D.J. (eds.) JELIA 1994. LNCS, vol. 838, pp. 365–378. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  15. 15.
    Ohlbach, H.J.: A resolution calculus for modal logics. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 500–516. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  16. 16.
    van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. Journal of the ACM 23(4), 733–742 (1976)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Linh Anh Nguyen
    • 1
  1. 1.Institute of InformaticsUniversity of WarsawWarsawPoland

Personalised recommendations