CAJ | 학술논문

Baratella定义了正规谓词逻辑程序的模态完全化语义,并证明了该语义关于SLDNF- 归结的部分完备性.本文首先给出了逻辑程序的模态直承算子,并研究了相关的理论性质, 进而证明了模态完全化语义关于SLDNF-归结的完备性.
Baratella정의료정규위사라집정서적모태완전화어의,병증명료해어의관우SLDNF- 귀결적부분완비성.본문수선급출료라집정서적모태직승산자,병연구료상관적이론성질, 진이증명료모태완전화어의관우SLDNF-귀결적완비성.
Baratella proposed a kind of modal completion for normal predicate logic programs 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 of this operator. Hence we give a direct proof for the completeness of SLDNF-res olution with respect to Baratella's completion.