【摘要】 Baratella定义了正规谓词逻辑程序的模态完全化语义 ,并证明了该语义关于 SL DNF-归结的部分完备性 .本文首先给出了逻辑程序的模态直承算子 ,并研究了相关的理论性质 ,进而证明了模态完全化语义关于 SL DNF-归结的完备性 .更多还原

【Abstract】 Baratella proposed a kind of modal completion for normal predicate logic program s and he partly proved that SLDNF resolution is complete with respect to his mo dal completion. In this paper,we introduce the modal form of immediate conse quence operator for logic programs and provide some interesting properties o f this operator. Hence we give a direct proof for the completeness of SLDNF res olution with respect to Baratella’s completion.更多还原