October 29, 1999
4:30pm

Ebenezer Ntienjem

Completion of Logic Programs with respect to Negation-As-Finite-Failure

The procedural semantics of logic programs, expressed by the so-called SLDNF-resolution, treats a variable occurring in a negative literal in the body but not in the head of a program clause as universally quantified whereas Clark's completion treats such a variable as existentially quantified. To close this gap between the declarative and procedural semantics of logic programs, we define a new approach to the completion of logic programs. To successfully define this new approach, we augment the syntax of a language for first-order predicate logic. We then compare this new approach with Clark's completion and with the partial completion of logic programs. We also relate the two-valued models of this completion of logic programs to rule-based inference systems.