Fixpoint semantics

The $T3_P$ definition given earlier can be applied when negative literals are present. It is equivalent to defining $T3_P(M)$ to be the interpretation such that the truth value for each atom $A$ is the truth value of $B$ in $M$, where $A \leftarrow B$ is a head clause instance in $comp(P)$. In the presence of negation $T3_P$ is generally not monotonic with respect to $T$ but is monotonic with respect to the information measure and, unlike $T_P$, at least one fixpoint exists and the $\subseteq_i$-least fixpoint can be built using $T3_P$ [FittingFitting1985].

For definite programs we introduced $T3^{+}_P$, which essentially overestimates the set of successful atoms. This is so even when negation is present -- a negated inadmissible atom is inadmissible and hence assumed to succeed (the negation makes no difference). When negation is present it is helpful to also have an operator which underestimates this set, by assuming inadmissible clause body instances fail:

Definition 14   $T3^{-}_P(M)$ is the interpretation such that an atom $A$ is

1. inadmissible, if $A$ is inadmissible in $M$,
2. true, if there is a clause instance $A \leftarrow B$ where $B$ is true in $M$,
3. false, otherwise.

As with $T3^{+}_P$, $T3^{-}_P$ generalises $T_P$ and its fixpoints include all those of $T_P$ and $T3_P$.