 \begin{slide}{} \slidetitle{Elimination of Negation in \fo\lp}
 
\bit
\item
Consider the following fragment of a Prolog program:

\[\begin{array}{l}
p(X,XS) \If member(X,XS) \If \ldots\\
p(X,XS) \If \neg member(X,XS) \If \ldots \vsk closed 
\vsk
member(X,X.XS).\\
member(X,Y.XS)\If member(X,XS)
\end{array}\]

\item
Last clause not a legal Horn clause: $\neg member(X,XS)$ not an atom.

\item Prolog solution: interpret $\neg$ as \emph{negation as 
failure}: ``$\neg A$ holds if $A$ \emph{finitely fails} to hold.

\item Problems (among others): an operational, not declarative notion 
which does not return answer substitutions:

\item Unsuitable for Logical Frameworks

\item Solution: eliminate negation through program transformation
\enit   \mends

 \begin{slide}{}
 \slidetitle{Elimination of Negation in \lp, $II$}

\[\begin{array}{l}
p(X,XS) \If member(X,XS) \If \ldots\\
p(X,XS) \If non\_member(X,XS) \If \ldots 
\vsk
member(X,X.XS).\\
member(X,Y.XS)\If member(X,XS)\vsk
non\_member(X,nil).\\
non\_member(X,Y.XS)\If diff(X,Y)\If non\_member(X,XS)
\end{array}\]where definition of \texttt{non\_member} has been synthesized by the user.


Aim: mechanize this transformation (when possible) so that for every 
ground $x,xs$:
\ben
\item
$def(member),def(non\_member)\vd member(x,xs)$ or 
$def(member),def(non\_member)\vd non\_member(x,xs)$
\item
It is not the case that both
$def(member),def(non\_member)\vd member(x,xs)$ and 
$def(member),def(non\_member)\vd member(x,xs)$
\enen\vfill
\end{slide}
