In this section we address the possibility of using the $DCA$ to limit the incompleteness of the transformation technique w.r.t.\ local variables.

$DCA$ depends on the signature $\Sigma$ of the underlying language. 
It essentially says that 
every element of the domain can be represented by a ground term 
of $\Sigma$.
\ie \beq
 (DCA): & \forall x(\bigvee\limits_{f \in \Sigma}
\exists \vec{y} (x=f(\vec{y}))) \eneq

First we extend the notion of covering to literals and relate it to an equivalent axiomatic version of CASE.

\begin{Def}[Covering]
Let $\| L\|$ be the set of ground instances of a literal $L$. A {\em 
covering\/} for $L$ is a set $\sigma_1 L, \dots, \sigma_n 
L$ such that $\| \sigma_1 L\| \cup \cdots\cup \| \sigma_n L \|  
\supseteq \| L \|$.
The instance of the $DCA$-schema corresponding to a covering for $L$ is:
\beq
CASE: & \forall(\forall y(\sigma_1 L \And \dots \And \sigma_n L) 
\Imp L)
\eneq
where $y$ are the new variables introduced by $\sigma_1, \dots, 
\sigma_n L$ (we assume that the range of every $\sigma_i$ 
contains only new variables that do not occur in $L$ or in the range 
of every other substitution). 
\end{Def}

 As usual, we
stipulate $\Sigma$  to be finite, being the signature of the 
underlying program. Moreover we will extend the notion of covering 
to arbitrary formulae, say in clausal form.

it needs to be formulated in all its generality.
\beq
CASE^*: & \forall(\forall y(\sigma_1 \phi \And \dots \And \sigma_n \phi) 
\Imp \phi)
\eneq



As we mentioned\footnote{to be expanded}, the original proposal in \cite{Bar90} was incomplete. The analysis in \cite{Mom95} of the interaction of the $DCA$ and the completion clarifies this fact\footnote{}.
\medskip
We 
associate to a program its failure axioms.  The starting point is the
only-if part of the completion of a predicate $p(\dots)$:
\[
\forall x(p(x) \Imp \bigvee\limits^n_{i=1}
\exists y_i(x=t_i \And
\bigwedge\limits^{h_i}_{k=1} L_{i,k}))\\
\]
For every $k_1,\dots, k_n$ such that $1 \leq k_i \leq h_i$
we infer 
\beq
& Fax_{k_1,\dots, k_n}(p): &  \forall x(p(x) \Imp \exists y 
\bigvee\limits^n_{i=1}
 (x=t_i \And L_{i,k_i}))\\
\eneq
By convention, the failure axiom of a unit clause introduces the 
constant {\em true}, hence $h_i \geq 1$ is always fulfilled.  Observe 
that these axioms contain {\em exactly} a singleton 
literal in every disjunct of the consequent. For a program $P$, 
$Fax(P)$ 
will indicate the set of its failure axioms in the latter sense, called  
{\em weak completion 
axioms}. The 
cardinality of  $Fax_{k_1,\dots, k_n}(p)$  is 
$\prod^n_{i=1} h_i$, where $n$
is the number of clauses and $h_i$ the number of literals in each 
clause of $P$ with head $p(\dots)$.

\begin{example}
\label{times}
The only-if part of $t$ (for {\em times}), the usual program for 
computing the product, is:
\begin{equation}\label{timecomp}
\begin{array}{lll}
\forall(t(a,b,c) \Imp  \exists x(a=x\And b=0\And c=0)  \Or \mbox{}\\
\quad \quad \quad \quad \quad \quad \exists x,y,z,w (a=x\And 
b=s(y)\And c=z \And t(x,y,w) \And 
sum(w,x,z)))\\
\end{array}
\end{equation}
From (\ref{timecomp}) we derive the failure axioms:
\[
\begin{array}{lllr}
\forall(t(a,b,c) \Imp\;\exists x,y,z,w &((a=x\And b=0\And c=0 \And 
true) \Or \mbox{} & \\
& (a=x\And b=s(y)\And c=z \And t(x,y,w))) &\\
\forall(t(a,b,c) \Imp \;\exists x,y,z,w &((a=x\And b=0\And c=0 \And 
true)  \Or \mbox{} & \\
& (a=x\And b=s(y)\And c=z  \And sum(w,x,z))) &\\
\end{array}
\]
\end{example} 

Note that, in general,
the conjunction of the $Fax_{k_1,\dots, k_n}(p)$
is notably weaker and does not imply the only-if part of 
$Comp(p)$. This is due to the shared binding of local variables, 
\ie those which appears in the body but not in the head of a 
clause---like $w$ in the former example. In the case of shared local 
variables, a factorization of failure axioms is needed. For example:

\begin{example}
By $DCA$, the right hand side of (\ref{timecomp}) is equivalent to 
the following factorization:
\[\begin{array}{l}
\exists x(a=x\And b=0\And c=0)  \Or \mbox{}\\
\exists x,y,z (a=x\And b=s(y)\And c=z \And t(x,y,0) \And 
sum(0,x,z))  \Or \mbox{}\\
\exists x,y,z,j (a=x\And b=s(y)\And c=z \And t(x,y,s(j)) \And 
sum(s(j),x,z))
\end{array}
\]
\begin{sloppypar}
\noindent
which corresponds to the fact that $w$ is covered by $0, s(j)$. We 
can derive four failure axioms from this factorization, parallel to 
the possible choices between $t(x,y,0),sum(0,x,z)$ in the second row 
and $t(x,y,s(j)),sum(s(j),x,z)$ (in the third one). For example, one of 
these axioms is:
\end{sloppypar}
\[
\begin{array}{lcl}
Fax1: & \forall(t(a,b,c) \Imp\;\exists x,y,z,j &((a=x\And b=0\And c=0 
\And 
true) \Or \mbox{} \\
& & (a=x\And b=s(y)\And c=z \And sum(0,x,z)) \Or \mbox{} \\
& &  (a=x\And b=s(y)\And c=z  \And t(x,y,s(j)))
\end{array}
\]
Notice that $\Not sum(0,0,s(v)); \Not t(0,0,s(j)) \in {\tt F}(\Not 
t(0,s(0),s(v)), Fax1)$. If you look at the finitely failed \SLD-tree for 
$\{  t(0,s(0),s(v))\}$, you can recognize that such finite failure is 
reduced  to the finite failure of $sum(0,0,s(v))$ and $\Not 
t(0,0,s(j))$.
\end{example}

Therefore, we will assume that local variables 
are restricted to occur only once in a literal in the body of a 
clause, similarly to condition {\em 
(d)} in Barbuti's definition of {\em flat} programs \cite{Bar90}. Remark that under this hypothesis the weak completion coincides 
with Clark's completion. 
Moreover we will assume, for the sake of the following two 
Theorems (\ref{failure} and \ref{t3}) 
%(and relative Appendix only) 
that the heads of clauses 
are {\em unrestricted}, or {\em left-linear},. 

\begin{Theorem}[Finite Failure]
\label{failure}
Given a  definite program $P$ and an atom $A$, 
if $P \cup \{ \If A\}$ has a finitely failed \SLD-tree, then there is 
a proof $\Pi :: \ \Not A$ in the
$F_{DCA}$-system applying only axioms from $Fax(P)$.
\end{Theorem}

Now we approach the relation  between finite failure and 
proofs in the $PF_{DCA}$-system.  To  every normal program $P$ we 
associate 
the set $WComp(P) = Ax(P) \cup Fax(P)$, where $Fax(P)$ has been 
straightforwardly extended to deal with literals.

\begin{Theorem}[$PF_{DCA}$/WComp(P) Adequacy]
\label{t3}
Let $P$ be a normal program and $L$ a literal. If there is a finitely 
failed \SLDNF-tree for $P \cup \{  \If L\}$, then there is a 
$PF_{DCA}$-proof $\Pi :: \ neg(L)$ with axioms from $WComp(P)$. If 
there is 
a \SLDNF-refutation of $P \cup \{  \If L\}$ with answer 
substitution $\delta$, 
then there is a   $PF_{DCA}$-proof $\Pi ::   \delta L$, with axioms 
from $WComp(P)$.
\end{Theorem}

\begin{Remark}
The proof enlightens the proviso on open literals. While no problem 
arises from $A_1,\dots,A_n$, were $B_1,\dots,B_m$ not ground, by 
inductive hypothesis we would get proofs $\Delta_1:: \q_1 
B_1,\dots,\Delta_m:: \q_m B_m$, and this would correspond to 
unsound substitutions of eigenvariables in $\Phi^*$.
\end{Remark}
To conclude, few observations are in order. 
\begin{itemize}
\item
$DCA$ is an axiom-schema, and therefore cannot be properly applied 
by an \aar.
 It could be  substituted  by the collection of all its instances, 
but this would give rise to infinitely many axioms. 
A working alternative is to introduce a systematic mechanism to 
generate
 deeper and deeper instances of the schema. This solution is similar 
to the {\tt herbrand} procedure of \cite{Bar90}. We will not develop 
this issue here. Our aim is to underline the {\em role of 
regularity\/}, which is an independent cause of the incompleteness 
of \SLDNF-resolution.
\item
According to the results of the Appendix, $DCA$ is not needed for 
two classes of programs. 
\begin{enumerate}
\item
Krom programs \cite{Kro}. In this case the body of a non-unit clause 
contains just one literal. In our following examples, we will 
consider mainly Krom programs.
\item
Left-linear programs without local variables. In this case, if $\Not 
A$ (with $A$ open) is a logical consequence of the completion, then 
there is a covering of $\Not A$ such that its elements have a $PF$-proof with axioms from the weak completion.
\end{enumerate}
\end{itemize}
