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 : 2iϕ → 2j 2kϕ) and I : 2iϕ → 2j ϕ. 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.

• Type: Conference
• Year: 2005
• Where: ICTAC
• Authors: Linh Anh Nguyen
• Keywords: ICTAC 2005, Modal Logic, Modal Logic Programs, Serial Multimodal Logics