A semantics for normal programs

When negation is introduced, many of the convenient properties of the semantics of logic programs break down. Typically model intersection properties no longer hold, the immediate consequence operator is no longer monotonic and in the procedural semantics negation is associated with finite failure which is dependent on the computation rule.

The first and simplest approach to negation was to use the negation as failure rule for the operational semantics and Clark's completion for the declarative semantics [ClarkClark1978]. Here we adapt this approach to our three-valued scheme.

Definition 8   Disjunctive normal programs are the same as disjunctive definite programs but they may have negated user-defined literals in the disjuncts.

The completion $comp(P)$ of a disjunctive normal program $P$ is the set of completions of clauses in $P$.

The completion of a clause $H \leftarrow B$ is $H \leftarrow \exists V_1 \exists V_2 \ldots B$, where the $V_i$ are the local variables.

The ``$\leftarrow$'' in completions is interpreted as ``if and only if'', modulo inadmissible atoms, in the model theory (see below). Clause instances of the form $\textbf{T} \leftarrow \textbf{F}$ are a source of incompleteness (a class of bugs called uncovered atoms [ShapiroShapiro1983]) which can translate to unsoundness when negation as failure is used. Clause instances of the form $\textbf{T} \leftarrow \textbf{I}$ can cause similar problems. Models of the completion therefore do not include such clauses. Clause instances of the form $\textbf{I} \leftarrow \textbf{F}$ and $\textbf{I} \leftarrow \textbf{T}$ do not to cause problems for Prolog. Even alternative execution mechanisms would not cause problems as long as the top level of the computation is assumed to be admissible or any inadmissible instances can be ignored. Due to the asymmetry with I we retain $\leftarrow$ instead of using $\leftrightarrow$.

One criticism of Clark's approach is that the completion may have no (two-valued) models. Adding a definition such as $p \leftarrow \neg p$ to a program results in everything being a logical consequence of the program but does not change the success set. Though we believe this criticism has been over-stated, it does not apply in the three-valued case. A three-valued model (and even strong model) always exists and an atom such as $p$ can be inadmissible, independent of the interpretation of the rest of the program.