% \def\vd{\null\mathrel{\vdash}} %Frank's
% \def\nprv{\null\mathrel{\not\vdash}} %Frank's
% \renewcommand{\prv}{\vd}
 \renewcommand{\mnot}{{\rm Not\ }}
\newcommand{\mnots}{{\rm Not^* }}
\renewcommand{\perp}{\bot}
%\newcommand{\mnotd}{{\rm Not}_{\mbox{$D$} }}
%\newcommand{\mnotg}{{\rm Not}_{{\mbox{$G$} }}}
\newcommand{\mnotd}{{\rm Not}_{\rm D}  }
\newcommand{\mnotg}{{\rm Not}_{\rm G}  }
\newcommand{\PP}{\cP^{+}}
\newcommand{\PM}{\cP^{-}}
\renewcommand{\sp}{\prv_{\cP}}
\newcommand{\spp}{\prv_{\PP}}
\newcommand{\snp}{\prv_{\PM}\mnotg }
\newcommand{\sn}{\prv_{\PM}}
\newcommand{\fpp}{\nprv_{\PP}}
\newcommand{\fnp}{\nprv_{\PM}\mnotg }
\newcommand{\fn}{\nprv_{\PM}}
\newcommand{\fp}{\nprv_{\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\tensor}{\oplus}
\newcommand{\ga}{ } %change!
\newcommand{\gna}{ }%change!
\newcommand{\vN}{\vec{N}}
\newcommand{\vM}{\vec{M}}
% \newcommand{\PA}{\mid \cP\cup\cA\mid_{\GG}}
\newcommand{\PA}{\mid \cP\mid}
\newcommand{\eqd}{\stackrel{\cdot}{=}}
\newcommand{\neqd}{\stackrel{\cdot}{\neq}}
\newcommand{\pix}{\Pi^{\cal X}}
\newcommand{\imm}{>\!\!>}
\newcommand{\nimm}{\imm}
% \newcommand{\nimm}{>\!<}
\newcommand{\IM}{{\cal I}^{-}}
\newcommand{\IP}{{\cal I}^{+}}
\newcommand{\SM}{{\cal S}^{-}}
\newcommand{\SP}{{\cal S}^{+}}


\section{The algebra of clause complementation}
\label{sec:alge}
Source language:
\beq
% Q & \bnfas & q\ \vM \mid \neg q\ \vM \mid \vM \eqd \vN\mid \vM \neqd 
% \vN\\
Q & \bnfas & q\ \vM \mid \neg q\ \vM \\
G & \bnfas & Q \mid G_{1}\And G_{2}\mid G_{1}\Or G_{2}\mid D\Imp G\mid
\Pi x:A.G\mid \vM \eqd \vN\mid \vM \neqd \vN\\
 %add \top\mid \perp
D & \bnfas & Q \mid \Pi x:A. D\mid Q \If G\mid D_{1}\And D_{2}\mid \top\mid
D_{1}\tensor D_{2}\mid \perp \\
% remove Q , since facts re Q \If\top
% \cP & \bnfas & \cdot\mid D,\cP
\eneq


\begin{Definition}[Universal Closure]
\label{def:uclos}
We define the \emph{universal closure $\pix(D)$ of a clause \wrt a 
set of bound variables $\cal X$} by induction on the structure of $D$:
\beq
\pix(\top) & = & \top\\
\pix(\perp) & = & \perp\\
\pix(D_{1} \And D_{2}) & = & \pix(D_{1}) \And \pix(D_{2})\\
\pix(D_{1} \tensor D_{2}) & = & \pix(D_{1}) \tensor \pix(D_{2})\\
% \pix(Q \If ) & = & \pix(D_{1}) \And \pix(D_{2})\\
\pix(\Pi x:A.D) & = & \Pi x:A. \Pi^{{\cal X}, x}(D)\\
\pix(Q \If G) & = & \Pi \xn. Q \If G\quad \xn = var(Q ) - {\cal X}
\eneq
\end{Definition}
This arguably awkward definition is tailored to normalized clauses 
\emph{without any local variables}.  It allows to define structurally 
the complement operation; in fact the complement of an atom can introduce 
new logical variables that must be universally quantified, while 
preserving the quantification status of the original ones.  Moreover 
the universal closure must be involutive.


\begin{Definition}[Clause Complementation]
\label{def:calgebra}
\beq
\mnotd (\top) & = & \perp\\
\mnotd(\perp) & = & \top\\
\mnotd ( D_{1}\And D_{2}) & = & \mnotd (D_{1}) \tensor \mnotd (D_{2})\\
\mnotd ( D_{1}\tensor D_{2}) & = & \mnotd (D_{1}) \And \mnotd (D_{2})\\
\mnotd (\Pi x:A. D) & = & \pix(\mnotd (D))\\
\mnotd(Q \If G) & = & \pix(\mnotd(Q ) \And \neg Q \If \mnotg(G)) \\
\mnotd( q\ \vM) & = & \pix(\BAnd_{\vN\in \mnot(\vM)} \neg (q\ \vN))
\eneq
where $\mnotg$ is defined on goals as follow:
\beq
\mnotg(G_{1}\And G_{2}) & = & \mnotg(G_{1}) \Or \mnotg(G_{2}) \\
% \mnotg(G_{1}\If G_{2}) & = & \mnotg(G_{1}) \Or \mnotg(G_{2}) \\
\mnotg(G_{1}\Or G_{2}) & = & \mnotg(G_{1}) \And  \mnotg(G_{2}) \\
\mnotg(D\Imp G) & = & D \Imp \mnotg(G) \\
\mnotg(\Pi x:A.G) & = & \Pi x:A. \mnotg(G) \\
\mnotg(Q) & = & \neg Q\\
\mnotg(\vM \eqd \vN) & = & \vM \neqd \vN\\
\mnotg(\vM \neqd \vN) & = & \vM \eqd \vN
\eneq
\end{Definition}

Given $m : Q \If G$,
%\footnote{We adopt for the moment the convention 
% that $G$ may be empty and $mnotg\cdot = \cdot$, instead of normalizing 
% facts, which is not economical}
we call $ \mnotd (m)$ the \emph{m-candidates}.  Candidates represent 
the potential negative contribution of each clause: the `factual' part 
$\mnotd(Q ) $ motivates failure due to clash with the head of $m$; the 
remainder $\mnotg (G)$ expresses failure in the body, if any.  Note 
that the latter only brings the body into what we may call 
\emph{parametric negation normal form}, to stress the distinction from 
classical negation normal form or even from normal form in 
constructive logics as extension of intuitionism with strong negation.  
Candidates from each clause in the definition of a predicate need to 
be considered simultaneously.  In fact, if an atom fails from its 
definition, then its negation must be provable from every $m$ 
candidate; symmetrically if a negative atom succeeds then its 
complement must fail from at least one candidate.  This is abstractly 
accomplished by the operator $\tensor$, which thus works similarly to 
disjunction.  Note that the former is available uniquely as a program 
constructor and can therefore be used only in the focusing phase of 
deductions.  This will allow to preserve the uniformity property.  In 
a second time, when describing the operational semantics of the system 
we will show how to `compile away' those disjunctions through an \ho 
version of the intersection operator described in \cite{MP90,Bar90}.

\begin{Lemma}
For every $D$, $\mnotd(D)$ is universally closed.
\end{Lemma}
\begin{proof}
A straightforward induction on the structure of $D$ confirms that every 
variable in $\mnotd(D)$ is in the scope of a universal quantifier.
\end{proof}

\begin{Corollary}[Program complementation]
\label{def:palgebra}
Let $def(q) = \BAnd_{i=1}^{n}( m_{i} : q\ \vM_{i} \If G_{i})$ be in 
$\cP$:
\beq
\mnotd(def(q)) & = & \bigoplus_{i=1}^{n} \mnotd(m_{i})\\
\mnotd(\cP) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnotd (def(q))
\eneq
\end{Corollary}
We abbreviate $\mnotd(def(q))$ in $def(\neg q)$.  As a special case, 
an undefined predicate $q$, \ie a predicate which occurs in a body of 
a clause but not as a head is represented by the empty conjunction 
$\top_q$.  Conversely $\perp_q$ denotes the universal definition for 
$q$.  We will forget the subscript in $\top_q$ and $\perp_{q}$, when it can be 
inferred by the context.  If $\PP$ is the source program, we use $\PM$ 
for $\mnotd (\PP)$.

\section{Success and Failure in Horn Logic}
% \newcommand{\vsk}{\\[2ex]}


Uniform proofs judgments:
\[
\begin{array}{ll}
\sp G & \mbox{Program $\cP$ uniformly entails $G$}\\
\fp G & \mbox{Program $\cP$ does \emph{not} uniformly entail $G$}\\
\sp D \imm Q & \mbox{Clause  $D$ immediately entails atom $Q$ under 
$\cP$}\\
\fp D \nimm Q & \mbox{Clause $D$ does \emph{not} immediately entail 
atom $Q$ under $\cP$}
\end{array}
\]


\input{sf-fig}

% \begin{figure}
% \label{fig:sf}
% \[
% \begin{array}{c}
% % |-
% % \ianc{}{}\ga\sp\top}{\top}\qquad\ianc{}{\gna\fp \perp}{S^{\nprv}_\perp}\vsk
% % top and bot
% \ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{S^{\prv}_{\eqd}}\qquad
% \ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{S^{\nprv}_{\eqd}}\vsk
% \ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{S^{\prv}_{\neqd}}\qquad
% \ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{S^{\nprv}_{\neqd}}\vsk
% \ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{S^{\prv}_\And}
% \qquad
% \ianc{\ga\fp G_1\quad\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{S^{\nprv}_\Or}
% \vsk
% \ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{S^{\prv}_{\Or_i}}
% \qquad
% \ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{S^{\nprv}_{\And_i}}
% % \qquad i\in 1\ \mbox{or} \ 2
% \vsk
% \ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{S^{\prv}_{ {\rm atm}}}
% \qquad
% \ianc{ \ga\fp def(Q) \nimm Q}{\ga\fp Q}{S^{\nprv}_{ {\rm atm}}}
% % \ianc{ \cP,G_{1}\prv_{u} G_{2}}{\cP\prv_{u} G_{1}\Imp G_{2}}{S^{\prv}_\Imp}
% % \qquad
% % \ianc{\cP\prv_{u} [a/x]G}{\cP\prv_{u}\Pi x. G}{S^{\prv}_\Pi^{*}}\vsk 
% \vsk
% % immediate >>
% \ianc{}{\ga\sp\perp\imm  Q}{I^{\prv}_\perp}\qquad
% \ianc{}{\ga\fp \top\nimm Q}{I^{\nprv}_\top}\vsk
% \ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{I^{\prv}_{\rm atm}}\qquad
% \ianc{\vN \neq \vM}{\ga\fp q\ \vN \nimm q\ \vM}{I^{\nprv}_{\rm atm}}\vsk
% \ianc{\mbox{for some $t:A$} \ \ga\sp  [t/x]D \imm Q}{\ga\sp \Pi x:A.D \imm Q}{I^{\prv}_\Pi}\qquad
% \ianc{\mbox{for all $t:A$} \ \ga\fp [t/x]D \nimm Q}{\ga\fp \Pi x:A.D \nimm Q}{I^{\nprv}_\Pi}\vsk
% \ianc{\ga\sp D_{i}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{I^{\nprv}_{\And_i}}\qquad
% \ianc{\ga\fp D_{i}\nimm Q}{\ga\sp D_{1}\tensor D_{2}\nimm Q}{I^{\nprv}_{\tensor_i}}\vsk
% \ianc{\ga\sp D_{1}\imm Q\quad \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm 
% Q}{I^{\prv}_\tensor}\qquad
% \ianc{\ga\fp D_{1}\nimm Q\quad \ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\And D_{2}\nimm
% Q}{I^{\nprv}_\And}\vsk
% \ianc{\sp G}{ \ga\sp (G\Imp Q) \imm Q}{I^{\prv}_\Imp}
% \vsk
% \ianc{\ga\sp \vN\neqd\vM}{\ga\fp (G\Imp q\ \vN) \nimm q\ \vM}{I^{\nprv}_{\Imp_1}}
% \qquad
% \ianc{\ga\sp \vN\eqd\vM\quad\fp G} {\ga\fp (G\Imp q\ \vN) \nimm q\ \vM}{I^{\nprv}_{\Imp_2}}
% % to avoid dependency pos-neg 
% % \ianc{\ga\sp Q'\imm Q\quad\sp G}{ \ga\sp (G\Imp Q') \imm Q}{I^{\prv}_\Imp}
% % \vsk
% % \ianc{\ga\fp Q'\nimm Q}{ \ga\fp (G\Imp Q') \nimm Q}{I^{\nprv}_{\Imp_1}}
% % \qquad
% % \ianc{\ga\sp Q'\imm Q\quad\fp G} { \ga\fp (G\Imp Q') \nimm Q}{I^{\nprv}_{\Imp_2}}
% \end{array}
% \]
% \caption{Provability and Denial in Horn Logic without existentials}
% \end{figure}

\begin{Lemma}
\label{le:clo-imm}
The following  are derived inference rules:
\[
\begin{array}{c}
\ianc{\mbox{for some $\q$ } \ \ga\sp\q D \imm Q}{\ga\sp\pix(D)\imm Q}
{I^{\prv}_{\pix}}
\qquad
\ianc{\mbox{for all $\q$ } \ \ga\fp\q D \nimm Q}{\ga\fp\pix(D)\nimm 
Q}{I^{\nprv}_{\pix}}
\end{array}
\]
\end{Lemma}
\begin{proof}
By induction on $D$.
\end{proof}

\begin{Lemma}
The following  are derived inference rules:
\[
\begin{array}{c}
\ianc{\ga\sp Q'\imm Q\quad\sp G}{ \ga\sp (G\Imp Q') \imm Q}{I'^{\prv}_\Imp}
\vsk
\ianc{\ga\fp Q'\nimm Q}{ \ga\fp (G\Imp Q') \nimm Q}{I'^{\nprv}_{\Imp_1}}
\qquad
 \ianc{\ga\sp Q'\imm Q\quad\fp G} { \ga\fp (G\Imp Q') \nimm Q}{I'^{\nprv}_{\Imp_2}}
\end{array}
\]
\end{Lemma}
\begin{proof}
Immediate.
\end{proof}

Note that in the above rules denial depends on provability, while this 
is not the case for the system in Figure \ref{fig:sf}. Still they make 
the main proof easier.

\begin{Lemma}
\label{le:part-imm}
\mbox{}
\ben
\item
If $\GG\prv \vM\in \|\mnot \vN\|$ then $\gna\sn\mnotd (q\ \vN) \imm \neg q\ \vM$
\item
If $\GG\prv \vM\not\in \| \mnot \vN\|$ then $\gna\fn\mnotd (q\ \vN) \nimm \neg q\ \vM$.
\enen
\end{Lemma}
\begin{proof}
\mbox{}
\ben
\item
Apply $I^{\prv} \And$ and $I^{\prv}_{\pix}$.
\item
Apply $I^{\prv} \And$ and $I^{\nprv}_{\pix}$.
\enen
\end{proof}


\begin{Proposition}[Exhaustivity]
If $\ga\fpp G$ then $ \gna\snp ( G)$.
\end{Proposition}
\begin{proof}
We generalize this to:
\ben
\item
If $\SM ::  \ga\fpp G$ then $\SP :: \gna\snp ( G)$.
\item
If for all substitutions $\sigma$ such that $dom(\sigma) = var(def(Q))$, 
$\IM :: \ga\fpp \sigma (def(Q)) \nimm Q$, then there is a substitution 
$\q$ such that $dom(\q) = var(def(\neg Q))$ and
$\IP :: \gna\sn \q (def(\neg Q)) \imm \neg Q$.
\enen
The proof is by mutual induction on $\SM$ and $\IM$\footnote{since 
substitutions are needed only in the $\Pi$ case we for now suppress mention to 
them in the other cases}.
% the structure of the judgments in \ref{fig:sf}
\bit
\item
Case: 
$$\IM = \ianc{}{\ga\fpp\top\nimm Q}{I^{\nprv}_\top}$$
If $\ga\fpp\top\nimm Q$ then $\mnotd (\top) = \perp$ and
$$ \IP = \ianc{}{\gna\sn\perp\imm \neg Q}{I^{\prv}_\perp}$$
\item
Case:
$$ \IM = \ianc{\ga\vN \neq \vM}{\ga\fpp q\ \vN \nimm q\ \vM}{I^{\nprv}_{\rm atm}}$$
From $\vN \neq \vM$ we infer $\GG\prv \vM\not\in\| \vN\|$.  By the 
term partition Lemma (\ref{le:part}) $\GG\prv \vM\in \|\mnot \vN\|$.  
By Lemma \ref{le:part-imm} $\gna\sn\mnotd ( q\ \vN) \imm\neg q\ \vM$.
\item
Case: $$ \IM = \ianc{\ga\fpp D_{i}\nimm Q}{\ga\fpp D_{1}\tensor 
D_{2}\nimm Q} {I^{\nprv}_{\tensor_i}}$$
For $i = 1 \mbox{ or } 2$.  By IH $\gna\sn \mnotd (D_{i})\imm \neg Q$ 
and by rule $S^{\nprv}_{\And_i}$ we infer $\gna\sn \mnotd (D_{1})\And 
\mnotd(D_{2})\imm \neg Q$ which, by definition of $\mnotd$, is 
equivalent to $\gna\sn \mnotd (D_{1}\tensor D_{2})\imm \neg Q$.
\item
Case: 
$$\IM = \ianc{\ga\fpp D_{1}\nimm Q\quad \ga\fpp D_{2}\nimm Q}{\ga\fpp D_{1}\And D_{2}\nimm 
Q}{I^{\nprv}_\And}$$
By IH $\gna\sn \mnotd (D_{1})\imm \neg Q$ and $\gna\sn\mnotd 
(D_{2})\imm \neg Q$, hence, by rule $I^{\prv}_\tensor$ we infer $ 
\gna\sn\mnotd (D_{1})\tensor \mnotd(D_{2})\imm \neg Q$ which, by 
definition of $\mnotd$, is equivalent to $ \gna\sn\mnotd (D_{1}\And 
D_{2})\imm \neg Q$.
\item
Case:
$$\IM = \ianc{\ga\fpp Q'\nimm Q}{\ga\fpp ( Q'\If G) \nimm Q}{I'^{\nprv}_{\Imp_1}}$$
By IH $\gna\sn\mnotd (Q') \imm \neg Q$ and by rule 
$S^{\nprv}_{\And_1}$ we have $\gna\sn(\mnotd (Q')\And \neg Q' \If 
\mnotg (G))\imm \neg Q$ which, by definition of $\mnotd$, is 
equivalent to $\gna\sn \mnotd(Q'\If G) \imm \neg Q$.
\item
Case: 
$$\IM = \ianc{\ga\spp Q'\imm Q \quad \fpp G}{\ga\fpp ( Q'\If G)
\nimm Q} {I'^{\nprv}_{\Imp_2}}$$
By IH $\snp (G)$ and $\ga\sn\neg Q'\imm \neg Q$.  Thus, by rule 
$I'^{\prv}_\Imp$ we have: $\gna\sn \neg Q' \If \mnotg (G)\imm \neg Q$ 
and rule $S^{\nprv}_{\And_2}$ yields $\gna\sn(\mnotd (Q')\And \neg Q' 
\If \mnotg (G))\imm \neg Q$ which, by definition of $\mnotd$, is 
equivalent to $\gna\sn \mnotd(Q'\If G) \imm \neg Q$.
\item
Case:
$$\IM = 
\ianc{\mbox{for all $t:A$} \ \ga\fpp [t/x]D \nimm Q}{\ga\fpp\Pi x:A.D \nimm Q}{I^{\nprv}_\Pi}$$
By IH there is a $\q$ such   that $\gna\sn\mnotd (\q D)\imm \neg Q$, hence by 
Lemma \ref{le:clo-imm}, $\gna\sn\pix (\mnotd(D))\imm\neg Q$ which, by definition of $\mnotd$, is equivalent to 
$\gna\sn\mnotd (\Pi x:A.D)\imm \neg Q$.
\item
Case:
$$\SM = \ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{S^{\prv}_{ {\rm 
atm}}}$$
By IH $\ga\snp def(\neg Q) \imm \neg Q$ which entails $\ga\snp (Q)$.
\item
Case: 
$$\SM = \ianc{\ga\fp G_1\quad\ga\fp G_{2}}{\ga\fp G_{1}\Or
G_{2}}{S^{\nprv}_\Or$$
By IH, $ \ga\snp (G_{1})$ and $\ga\snp (G_{2})$ which implies $\ga\sn 
\mnotg (G_{1})\And \mnotg (G_{2})$, which is equivalent, by definition 
of $\mnotg$, to \ga\snp (G_{1} \Or G_{2})$.
\item
Case: 
$$\SM =
\ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{S^{\nprv}_{\And_i}}$$
For $i=1 \mbox{ or } 2$.  By IH $ \ga\snp (G_{i})$ which implies 
$\ga\sn \mnotg (G_{1})\Or \mnotg (G_{2})$, which is equivalent, by 
definition of $\mnotg$, to $ \ga\snp (G_{1} \And G_{2})$.
\item
Case:
$$ \SM =
\ianc{\vM \not = \vN}{\ga\fpp \vM \eqd \vN}{S^{\nprv}_{\eqd}}$$
Then $\ga\sn  \vM \neqd \vN$ and $\ga\sn\mnotg( \vM \eqd \vN)$.
\item
Case:
$$ \SM =
\ianc{\vM  = \vN}{\ga\fpp \vM \neqd \vN}{S^{\nprv}_{\neqd}}$$
Then $\ga\sn\vM \eqd \vN$ and $\ga\sn\mnotg( \vM \neqd \vN)$.
\enit
\end{proof}

\begin{Proposition}[Disjointness]
If $\ga\spp G$ then $\gna\fnp ( G)$.
\end{Proposition}
\begin{proof} We generalize this to:
\ben
\item
If $\SP ::  \ga\spp G$ then $\SM :: \gna\fnp ( G)$
\item
If there is a substitution $\sigma$ such that 
$dom(\sigma)=var(def(Q))$ and 
$\IP :: \ga\spp \sigma (def(Q)) \imm Q$ then 
for all substitutions $\q$ such that $dom(\q)=var(def(\neg Q)),\  \IM :: 
\gna\fn \q (def(\neg Q)) \nimm \neg Q$.
\enen
The proof is by induction on the structure of $\SP$ and $\IM$\footnote{since 
substitutions are needed only in the $\Pi$ case we for now suppress mention to 
them in the other cases}.
\bit
\item
Case: 
$$\IP = \ianc{}{\ga\spp\perp\imm Q}{I^{\prv}_\perp}$$
Then $\mnotd (\perp) = \top$ and
 $$ \IM = \ianc{}{\gna\fn\top\nimm \neg Q}{I^{\nprv}_\top}$$
\item
Case:
$$ \IP = \ianc{\ga\vN = \vM}{\ga\spp q\ \vN \imm q\ \vM}{I^{\prv}_{\rm atm}}$$
From $\vN = \vM$ we infer $\GG\prv \vM\in\| \vN\|$. By the term partition 
Lemma (\ref{le:part}) $\GG\prv \vM\not\in \|\mnot \vN\|$. By Lemma 
\ref{le:part-imm} $\gna\fn\mnotd (q\ \vN) \nimm\neg q\ \vM$.
\item
Case:
$$ \IP = \ianc{\ga\spp D_{i}\imm Q}{\ga\spp D_{1}\And D_{2}\imm Q}{S^{\nprv}_{\And_i}}$$
For $i = 1 \mbox{ or } 2$.  By IH $\gna\fn\mnot D_{i}\nimm \neg Q$ and by rule 
$I^{\nprv}_{\tensor_i}$ we infer $\gna\fn\mnotd (D_{1})\tensor \mnot(D_{2})\nimm \neg Q$
which, by definition of $\mnotd$, is equivalent to  $\gna\fn\mnotd (D_{1}\And D_{2})\nimm \neg Q$.
\item
Case: 
$$\IP = \ianc{\ga\spp D_{1}\imm Q\quad D_{2}\imm Q}{\ga\spp D_{1}\tensor D_{2}\imm 
Q}{I^{\prv}_\tensor}$$
 By IH $\gna\fn\mnotd (D_{1})\nimm \neg Q$ and 
$\gna\fn\mnotd (D_{2})\nimm \neg Q$, hence, by rule $I^{\nprv}_\And$ we infer
$\gna\fn \mnotd (D_{1})\And\mnotd(D_{2})\nimm \neg Q$
which, by definition of $\mnotd$, is equivalent to  $\gna\fn \mnotd (D_{1}\tensor D_{2})\nimm \neg Q$. 
\item
Case:
$$\IP = \ianc{\ga\spp Q'\imm Q \quad \spp G}{ \ga\spp (Q' \If G) \imm 
Q}{I'^{\prv}_\Imp} $$
By IH $\gna\fn\mnotd (Q') \nimm \neg Q$ and $\fnp (G)$.  Rule 
$I'^{\nprv}_{\Imp_1}$ yields $\neg Q' \If \mnotg (G)\nimm Q$: finally 
by rule $I^{\nprv}_\And$ we have $\gna\fn(\mnotd (Q')\And \neg Q' \If 
\mnotg (G))\nimm Q$ which is equivalent to $\gna\fn \mnotd(Q'\If 
G)\nimm \neg Q$.
\item
Case:
$$\IP = 
\ianc{ \ga\spp [t/x]D \imm Q}{\ga\spp \Pi x:A.D \imm Q}{I^{\prv}_\Pi}$$
By IH for all $\q$ such that $\gna\fn\mnotd (\q D)\nimm \neg Q$, 
hence by Lemma \ref{le:clo-imm}, $\gna\fnp\pix (\mnotd(D))\nimm\neg 
Q$ which, by definition of $\mnotd$, is equivalent to $\gna\fn\mnotd 
(\Pi x:A.D)\nimm \neg Q$.
\item
Case:
$$\SP =
\ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{S^{\prv}_{ {\rm atm}}}$$
By IH $\gna\fn def(\neg Q) \nimm \neg Q$  which entails $\ga\fnp (Q)$. 
\item 
Case:
$$\SP = \ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And 
G_{2}}{S^{\prv}_\And}$$
By IH, $ \ga\fnp(G_{1})$ and $\ga\fnp (G_{2})$ which implies $\ga\fn 
\mnotd (G_{1}) \Or \mnotd(G_{2})$ which, by definition of $\mnotg$, 
is equivalent to $ \ga\fnp (G_{1} \And G_{2})$.
\item
Case: 
$$\SP = \ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{S^{\prv}_{\Or_i}}
$$
For $i=1 \mbox{ or } 2$.  By IH, $ \ga\fnp (G_{i})$ which implies 
$\ga\fn \mnotd (G_{1}) \And \mnotd(G_{2})$ which, by definition of 
$\mnotg$, is equivalent to $ \ga\fnp (G_{1} \Or G_{2})$.
\item
Case:
$$ \SP =
\ianc{\vM = \vN}{\ga\spp \vM \eqd \vN}{S^{\prv}_{\eqd}}$$
Then $\ga\fn  \vM \neqd \vN$ and $\ga\fn\mnotg( \vM \eqd \vN)$.
\item
Case:
$$ \SP =
\ianc{\vM \not = \vN}{\ga\spp \vM \neqd \vN}{S^{\nprv}_{\eqd}}$$
Then $\ga\fn  \vM \eqd \vN$ and $\ga\sn\mnotg( \vM \neqd \vN)$.
\enit
\end{proof}

%%%%%%%%%

\section{Elimination of $\tensor$}

We now show how to eliminate the $\tensor$ operator preserving 
provability and denial.  We generalize the approach in 
\cite{MP90,Bar90}, where the operation was defined as follows:
for $m1: P_{1}\If G_{1}$ and  $m2: P_{2}\If G_{2}$:
\beq
m1 \tensor m2 & = &  \q(P_{1}\If G_1\And G_2) \quad\mbox{{\rm where }} \q = mgu(P_{1},P_{2}) 
\eneq
Yet, this definition is not quite adequate to our setting:
\bit
\item
Strict unification and more in general \ho   unification is not unary.
\item
We will have to take into account parameter (dis)equations, as well as 
closed (dis)equations stemming from left-linearization.
\enit

We thus choose to compile our source into an intermediate language 
which makes unification problems explicit as simple equational problems 
in the style of the unification logic introduced in \cite{Pfenning91lf}.  
In a further system we will show how to perform constraint 
simplification as used in \emph{Elf}  \cite{Pfenning89lics} and 
\emph{Twelf} \cite{Schuermann98cade}.

\newcommand{\eprv}{\stackrel{\prv}{\sim}}
\newcommand{\enprv}{\stackrel{\nprv}{\sim}}
\smallskip

We introduce a notion of \emph{operational equivalence} \wrt 
provability and denial: note that equivalence \wrt denial requires 
some sophistication in the notion of `allowed' goal whenever embedded 
implications are introduced.  This is essentially due to the 
non-admissibility of cut in the negative system, discussed in Section 
\ref{lamrelated}.

\begin{Definition}[Operational Equivalence]
\label{def:opeq}
\mbox{}
\bit
\item
We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent \wrt 
provability}, denoted $\cP_{1}\eprv \cP_{2}$, iff, for any goal $G$ we 
have $\ga\prv_{\cP_{1}} G$ iff $\ga\prv_{\cP_{2}} G$.
\item
We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent \wrt 
denial}, denoted $\cP_{1}\enprv \cP_{2}$, iff, for any goal $G$ we have 
$\ga\nprv_{\cP_{1}} G$ iff $\ga\nprv_{\cP_{2}} G$.
\item
We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent}, 
denoted $\cP_{1}\sim \cP_{2}$, iff $\cP_{1}\eprv \cP_{2}$ and 
$\cP_{1}\enprv \cP_{2}$.  
\enit
\end{Definition}

\begin{Lemma}
\label{le:exchng}
$D_{1}\tensor D_{2}\sim D_{2}\tensor D_{1}$.
\end{Lemma}
\begin{proof}
Trivial.
\end{proof}

% It is convenient to bring the source program in a sort of conjucntive 
% normal form , so that

We adapt the \emph{residuation} technique used in \cite{Pfenning?} to 
compile immediate implication into resolution.  We define the judgment 
$D_{1}\tensor D_{2} \setminus D$ by induction on (normalized) $D_{1}$, 
with the intended meaning of `$D_{1}\tensor D_{2}$ compiles to $D$':

\begin{Lemma}
\label{le:imm-eq}
The following are valid rules of inference:
$$\ianc{\ga\sp q\ \vN_{1}\imm Q\quad \vN_{1}\eqd \vN_{2}}{\ga\sp q\ \vN_{2}\imm Q}{\imm\eqd}
\qquad
\ianc{\gna\fp q\ \vN_{1}\nimm Q\quad \vN_{1}\neqd \vN_{2}}{\ga\fp q\ \vN_{2}\nimm Q}{\imm\neqd}
$$
\end{Lemma}
\begin{proof}
It will be trivial once we specify the equality rules.
\end{proof}

\begin{figure}
\label{fig:otimes}
\[
\begin{array}{c}
\ianc{}{\top\tensor D \setminus \top}{\setminus\top}
\vsk
\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}}{\setminus{\rm 
atm}}\vsk
\ianc{D\tensor (Q\If G)\setminus D'}{(Q\If G)\tensor D\setminus D'}
{\setminus{\rm exc}}
\qquad
\ianc{([t/x] D_{1})\tensor D_{2}\setminus[t/x]D}{(\Pi x:A.D_{1})\tensor 
D_{2}\setminus \Pi x:A. D}{\setminus\Pi}\vsk
\ianc{D_{1}\tensor D_{2}\setminus D\quad D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\And D'_{1})\tensor D_{2}\setminus D\And D'}{\setminus\And}
\end{array}
\]
\caption{Judgment $D_{1}\tensor D_{2}\setminus D$}
\end{figure}

The following guarantees that compilation preserves immediate 
entailment.

\begin{Lemma}
\label{le:te-tim}
$ D_{1}\tensor D_{2}\setminus D$ and $D\imm Q$ iff $D_{1}\tensor D_{2} \imm Q$.
\end{Lemma}
\begin{proof}
By induction on $D_{1}$. We show only some significant cases:
\bit
\item
Case:
$$\ianc{}{\top\tensor D \setminus \top}{\setminus\top}$$
and $\ga\sp\top\imm Q$ iff falsehood iff $\ga\sp\top\imm Q$ and 
$\ga\sp D\imm Q$ iff $\ga\sp\top\tensor D\imm Q$.
\item
Case:
$$\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}}{\setminus{\rm 
atm}}$$
From $\ga\sp q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And 
G_{2}\imm Q$, by inversion follows $\ga\sp q\ \vN_{1}\imm \And 
\vN_{1}\eqd \vN_{2}\And G_{1}\And G_{2}$ iff by Lemma \ref{le:imm-eq} 
$\ga\sp q\ \vN_{2}\imm Q$ iff $\ga\sp q\ \vN_{1}\If G_{1}\imm Q$ and 
$\ga\sp q\ \vN_{2}\If G_{2}\imm Q$ iff $\ga\sp q\ \vN_{1}\If 
G_{1}\tensor q\ \vN_{2}\If G_{2}\imm Q$.
\item
Case:
$$\ianc{([t/x] D_{1})\tensor D_{2}\setminus [t/x]D}{(\Pi x:A.D_{1})\tensor 
D_{2}\setminus \Pi x:A. D}{\setminus\Pi}$$
By inversion $([t/x] D_{1})\tensor D_{2} \setminus[t/x]D$ and $\ga\sp 
[t/x]D\imm Q$ which is equivalent by IH to $\ga\sp [t/x]D_{1}\tensor 
D_{2}\imm Q$ iff $\ga\sp [t/x]D_{1}\imm Q$ and $\ga\sp D_{2}\imm Q$ 
iff $\ga\sp (\Pi x:A.D_{1})\tensor D_{2}\imm Q$.
\item
Case:
$$\ianc{D\tensor (Q\If G)\setminus D'}{(Q\If G)\tensor D\setminus D'}
{\setminus{\rm exc}}$$
It follows by a direct appeal to the inductive hypothesis using 
Lemma \ref{le:exchng}.
\enit
\end{proof}

The following guarantees that compilation preserves immediate denial.  
Note that we have to take into account the meta-level universal 
quantification on terms brought in by the $I^{\nprv}_{\Pi}$ rule.

\begin{Lemma}
\label{le:te-nimm}
For all $\q, \ \q D_{1}\tensor D_{2}\setminus D$ and $\q D\nimm Q$ iff 
$\q D_{1}\tensor D_{2} \nimm Q$.  
\end{Lemma}
\begin{proof}
By induction on $D_{1}$.  We avoid mentioning substitutions when they 
are immaterial and show only some significant cases in the $\Imp$ 
direction, the converse following the same lines.
\bit
\item
Case:
$$\ianc{}{\top\tensor D \setminus \top}{\setminus\top}$$
$\ga\sp\top\nimm Q$ obviously entails   $\ga\sp\top\tensor D\nimm Q$.
\item
Case:
$$\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}}{\setminus{\rm 
atm}}$$
Assume $\ga\fp q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And 
G_{2}\nimm Q$.  Then either $\ga\fp q\ \vN_{1}\nimm Q$ or $\ga\fp 
\vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}$. The first case entails
$\ga\fp q\ \vN_{1}\nimm Q$ or $\ga\fp G_{1}$ which implies 
$\ga\fp q\ \vN_{1}\If G_{1}\nimm Q$ and finally 
$\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. The 
second horn splits into three subcases:
\ben
\item
$\vN_{1}\neqd \vN_{2}$. By Lemma \ref{le:imm-eq} $\ga\fp q\ 
\vN_{2}\nimm Q$ which implies $\ga\fp q\ \vN_{2}\If G_{2}\nimm Q$ and finally 
$\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
\item
$\ga\fp G_{2}$ implies $\ga\fp q\ \vN_{2}\If G_{2}\nimm Q$ and finally 
$\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
\item
$\ga\fp G_{1}$ implies $\ga\fp q\ \vN_{1}\If G_{1}\nimm Q$ and finally 
$\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
\enen
\item
Case:
$$\ianc{([t/x] D_{1})\tensor D_{2}\setminus [t/x] D}{(\Pi x:A.D_{1})\tensor 
D_{2}\setminus \Pi x:A. D}{\setminus\Pi}$$
From $([t/x] D_{1})\tensor D_{2}\setminus [t/x] D$ and $\ga\sp \q 
D\nimm Q$ by IH we infer $\ga\sp \q D\tensor D_{2}\nimm Q$, 
equivalent to $\ga\sp \q D\nimm Q$ or $ D_{2}\nimm Q$ which implies 
$(\Pi x:A.D_{1})\tensor D_{2}\nimm Q$. 
\enit
\end{proof}

\newcommand{\PT}{\tensor\cP}

We now define the effect of the above compilation on a program:
\begin{Definition}
\label{def:tensorpro}
\beq
\mid \top\mid_{\tensor} & = & \top\\
\mid \perp\mid_{\tensor} & = & \perp\\
\mid Q\If G\mid_{\tensor} & = & Q\If G\\
\mid D_{1}\And D_{2} \mid_{\tensor} & = & \mid D_{1} 
\mid_{\tensor}\And \mid D_{2} \mid_{\tensor} \\
\mid \Pi x:A.D \mid_{\tensor} & = & \Pi x:A. \mid D \mid_{\tensor} \\
\mid D_{1}\tensor D_{2} \mid_{\tensor} & = & \mid D \mid_{\tensor} 
\quad \mbox{\textrm{where }} D_{1}\tensor D_{2} \setminus D
\eneq
\end{Definition}

We abridge $\mid \cP\mid_{\tensor}$ in $\PT$.

\begin{Proposition}
\label{ppn:te-imm}
$\cP \eprv \PT$.
\end{Proposition}
\begin{proof}
We need to show $\ga\prv_{\cP} G$ iff $\ga\prv_{\PT} G$. We 
generalize this to:
\ben
\item
$\SP :: \ga\sp G$ iff $\tensor \SP :: \ga\prv_{\PT} G$;
\item
$\IP :: \ga\sp def(Q) \imm Q$ iff $\tensor \IP :: \ga\prv_{\PT} 
def(Q) \imm Q$.
\enen
The proof is a straightforward mutual induction on the structure of the 
derivation using Lemma \ref{le:te-tim}.
\end{proof}

\begin{Proposition}
\label{ppn:te-nimm}
$\cP \enprv \PT$.
\end{Proposition}
\begin{proof}
We need to show $\ga\nprv_{\cP} G$ iff $\ga\nprv_{\PT} G$. We 
generalize this to:
\ben
\item
$\SM :: \ga\fp G$ iff $\tensor \SM :: \ga\nprv_{\PT} G$;
\item
For every $\q$, $\IM :: \ga\fp \q(def(Q)) \nimm Q$ iff $\tensor \IM :: \ga\nprv_{\PT} 
\q(def(Q)) \nimm Q$.
\enen
The proof is a straightforward mutual induction on the structure of the 
derivation using Lemma \ref{le:te-nimm}.
\end{proof}

From the above propositions, we have the soundness and completeness 
of the compilation:

\begin{Corollary}
\label{co:te-ti}
$\cP \sim \PT$.
\end{Corollary}