An SLD-resolution calculus for basic serial multimodal logics

Abstract

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. © Springer-Verlag Berlin Heidelberg 2005.