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

摘要: We propose a modal logic programming language called MProlog, which is as expressive the general Horn fragment. give fixpoint semantics and an SLD-resolution calculus for MProlog in all of basic serial logics KD, T, KDB, B, KD4, S4, KD5, KD45, S5. For program P L being one mentioned logics, we define operator T_{L,P}, has least I_{L,P}. This set formulae, may contain labeled forms d, L-model generator P. The standard model I_{L,P} shown to be designed with similar style classical programming. It sound complete. also extend almost KB, K5, K45, KB5.