Model-theoretic semantics

We define models for the completion of a program. First, negation is defined by $\neg \textbf{T} = \textbf{F}, \neg \textbf{F} = \textbf{T}, \neg \textbf{I} = \textbf{I}$. The existential quantification of a closed formula is $\textbf{T}$ if any instance is $\textbf{T}$, $\textbf{F}$ if all instances are $\textbf{F}$, and $\textbf{I}$ otherwise.

Definition 12 (model of $comp(P)$)   An interpretation is a model of $comp(P)$ if it is a model of every clause in $comp(P)$.

An interpretation is a model of $H \leftarrow B$ if for all head instances $H \theta \leftarrow B \theta$, if $H \theta$ is T then $\exists(B \theta)$ is T and if $H \theta$ is F then $\exists(B \theta)$ is F in the interpretation.

That is, we avoid clause instances of the form $\textbf{F} \leftarrow \textbf{T}$, $\textbf{F} \leftarrow \textbf{I}$, $\textbf{T} \leftarrow \textbf{F}$ and $\textbf{T} \leftarrow \textbf{I}$. The first two cases can cause unsoundness for definite clauses, as discussed earlier. The last two cases can cause unsoundness with negation as failure. Note that we only consider instantiation of head variables and use existential quantification in the bodies. We allow the case where the instance of $H$ is $\textbf{T}$ and some but not all corresponding instances of $B$ are $\textbf{T}$ (corresponding to a true atom with a legitimate proof and one or more suspect proofs which use inadmissible or false atoms). Adapting the definite clause model definition in a simpler way results in a stronger definition of a model, unnecessarily rejecting some programs for a given interpretation.

To summarise, the declarative semantics we propose for logic programs is Clark's completion with Kleene's strong three-valued logic used for the right sides of the arrow and the following truth table used for the arrow.

$\leftarrow$	T	F	I
T	T	F	F
F	F	T	F
I	T	T	T

The model intersection properties stated earlier do not generally hold for disjunctive normal programs. We define strong models of completions in the typical way (see [Apt and BolApt and Bol1994]), additionally avoiding clauses of the form $\textbf{I} \leftarrow \textbf{T}$ and $\textbf{I} \leftarrow \textbf{F}$:

Definition 13 (strong model of $comp(P)$)   An interpretation $M$ is a strong model of $comp(P)$ if every head clause instance has the same truth value for the head and body in $M$.

Our intended interpretation of merge/3 is not a strong model even if extra tests are added. Clauses such as merge([], Bs, Bs) :- sorted_list(Bs) have instances where the head is I and the body is F. Strong models must precisely specify the behaviour of all predicates.