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.
['Linh Anh Nguyen']
An SLD-resolution calculus for basic serial multimodal logics