ON THE COMPLETED DATABASE SEMANTICS FOR NEGATION  

作　　者：沈一栋 程代杰 童頫 SOENEN R. TAHON C. 

机构地区：[1]Department of Computer Science, Chongqing University, Chongqing 630044, PRC [2]Department of Computer Science, Shanghai University of Science and Technology, Shanghai 201800, PRC [3]L.G. I. L, URIAH-CNRS N#1118, Universitè de Valenciennes, 59326 Valenciennes, France

出　　处：《Science China Mathematics》1992年第12期1516-1528,共13页中国科学：数学（英文版）

基　　金：Project supported by the National Natural Science Foundation of China and in part by University of Valenciennes under the cooperation agreement with Chongqing University

摘　　要：As a semantics for negation, the completed datsbase appears to be a little too strong.It makes no sense when it is ineonsistent. However, as has been shown by Shepherdson, the general problem of determining whether the completed database is codaistent is recursively undecidable. In this paper, we present a necessary and sufficient condition for the consistency of the completed database and use it to prove the consistency of the completed database for definite, locally stratified and R-terminable programs, respectively. We then establish a weak version of the completed database semantics for negation. Informally, the semantics says that for any function-free logic program P the results inferred by applying the SLDNF-refutation procedure via the "Latest-first" computation rule are logical consequences of the relevant completed database comp(REL(P)),where comp(REL(P))is always consistent ever if comp(P)is ineonsistent.As a semantics for negation, the completed datsbase appears to be a little too strong.It makes no sense when it is ineonsistent. However, as has been shown by Shepherdson, the general problem of determining whether the completed database is codaistent is recursively undecidable. In this paper, we present a necessary and sufficient condition for the consistency of the completed database and use it to prove the consistency of the completed database for definite, locally stratified and R-terminable programs, respectively. We then establish a weak version of the completed database semantics for negation. Informally, the semantics says that for any function-free logic program P the results inferred by applying the SLDNF-refutation procedure via the 'Latest-first' computation rule are logical consequences of the relevant completed database comp(REL(P)),where comp(REL(P))is always consistent ever if comp(P)is ineonsistent.

关 键 词：NEGATION AS FAILURE the completed DATABASE consistency. 

分 类 号：N[自然科学总论]