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

Article type: Research Article

Authors: Nguyen, Linh Anh

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

Abstract: 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 least L-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.

Keywords:

Journal: Fundamenta Informaticae, vol. 55, no. 1, pp. 63-100, 2003