ON THE COMPLETED DATABASE SEMANTICS FOR NEGATION

As a semantics for negation. the completed database appears to be a little too strong. It makes no sense when it is inconsistent. However, as has been shown by Shepherdson, the general problem of determining whether the completed database is consistent 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 even if comp(P) is inconsistent.