
\section{Disunification}
\label{sec:disunif}
Disunification is devoted to solving {\bf arbitrary} first order 
formulae
whose only predicate symbol is equality, call them {\em equational 
formulae}.  The definition of what a {\em solution} is differs on the 
application at hand. We may be interested only in the overall 
validity or in the possible assignments that make the formula valid. 

\smallskip
From an historic perspective this field became defined when it was 
realized by Martelli \& Montanari (if not by Herbrand) that 
\fo-unification can be seen as a transformation on set of equations. 
On the other hand the work of 
Mal'cev \cite{Mal71} on the decidability and complete axiomability of 
the theory of equational algebrae is clearly an ancestor.

The definition of Prolog-II introduced disequation. Indeed Colmerauer 
\cite{Col84} showed them to have solutions in the algebra of rational 
trees.
Next
Lassez et Marriot \cite{Las87} proposed the seminal (although 
awkward) {\em uncover} algorithm  for computing relative 
complements.
% of linear first-order terms
%\footnote{Definition in chapter 1, discussion in~\ref{bnot}.} 
As we have seen, those problems are systems of disequation with 
universally quantified variables.

Kirchner and Lescanne first unified those previous papers in the 
framework of equational problems and proposed a set of 
transformational rules, though without a completeness proof
\cite{Kir87}.

Maher introduced the unification community to Mal'cev's results 
\cite{Mah88}. Comon and Lescanne were the first one to present an adequate set of 
rules \cite{Com88,CL89} and the former surveyed the field \cite{Com91}.
% Now this has become a fast growing 
% area in its own which
% is impossible to review here: extension of disunification in 
% order-sorted signatures is under research as well as in the presence 
% of specific equational theories, inequalities   and symbolic 
% constraints. We will be
% presenting only what is required for our ultimate goal. 

%\subsection{A Preliminary Account of Disunification}
How to go on to derive a disunification procedure can therefore vary 
from the syntax and semantics we are concerned with, but 
nevertheless it entails the following steps:
\bit
\item
Provide a set of axioms $\cal T$ that hold in the model we consider
\item
Design a set of rules $\cal R$ for the transformation of equational 
formulae that can be proven correct w.r.t.\ $\cal T$
\item
Design a control $C$ on $\cal R$ such that the application of rules 
satisfying $\cal R$ terminates: irreducible formulae are in solved 
form and have the same set of solutions of the original problem
\item
If arbitrary formulae are allowed and solved form are trivially 
decidable, this entails the decidability and completeness of $\cal T$.
\enit

The simplest example is unification of finite (first-order) terms: 
\bit
\item
 $\cal T$ is Clark's free equality theory \cite{Cla78}.
\item ${\cal R}$ are, say, the Martelli-Montanari rules
  \cite{Martelli76};
correctness corresponds to the 
preservation of solutions under rule application, or it can be 
refined into the content of Clark's lemma
\item
 Solved forms yield idempotent substitutions (see definition 
\ref{sf}) and control restricts the application of variable 
elimination. Completeness (of the theory) is established for example 
as in \cite{Mah88}.
\enit

The disunification rewrite rules are divided in three big chunks:
\bit
\item
Equality rules, \ie rules which are correct for any equational algebra
\item 
Rules for finite trees over any signature
\item 
Rules for finite trees over a finite signature.
\enit

We will not present the complete set of rules with 
logical provisos and control.  We 
just mention that the first group contains  Replacement, 
 Universal Quantifier  Elimination,  Existential 
quantifier  Elimination  and  Elimination of  
Disjunctions.
The second batch  contain  Clash,  Decomposition,  
Occur check. The third section would contain rules which are sensitive 
to the cardinality of the signature. Here we mention only
the  Explosion rule, which is clearly motivated by the domain closure
axiom ($DCA$) \cite{Mancarrella88}.

We list below the rules relevant to the following example in their 
barest form, \ie with only soundness and no termination condition:


\begin{figure}[htbp] 
\label{fig:fo-disunif}
\[
\fbox{$\vspace{2em}
\begin{array} {lllll}
R & : & w=t \And P[w] & \Lmap & w=t \And [t/w]P\\
M1 & : & w=t \And w\not=u & \Lmap & w=t \And t\not = u\\
UE1 & : & \forall \vy,y : P \And y \neq t & \Lmap & \bot\\
% % UE2 & : & \forall \vy,y   : P \Or y \neq t & \Lmap & \forall \vy  : 
% [t/y] P\footnote{Used?}
% \\
Clh(T) & : & f(\tn) \nq g(\sm) & \Lmap & \top\\
Clh(F) & : & f(\tn) = g(\sm) & \Lmap & \bot\\
Dec1 & : & f(\tn) \neq f(\un) & \Lmap & \BOr\limits^{n}_{i=1} t_i \neq 
u_i\\
Dec2 & : & f(\tn) = f(\un) & \Lmap & \BAnd\limits^{n}_{i=1} t_i = 
u_i\\
E & : & \forall \vy : P & \Lmap & \BOr\limits_{f \in \Sigma} (\exists 
\vx \forall \vy : P \And w  = f(\vx))
\end{array}
$}
\]
In  $R$ $w \not \in Var(t)$, in  $E$, $P$ contains a 
(dis)equation with LHS $w$ and RHS $u$, where the latter is not a 
variable and contains a parameter.
\caption{Some disunification rules with minimal proviso}
\end{figure}

Thus a disunification algorithm over finite trees will solve 
complement problems, eventually providing values for free 
variables.

\medskip

We now give an example of disunification on the numerals signature,
which is required in the synthesis of the {\tt odd} program. It 
consists in  solving 
\begin{eqnarray}
\label{eqb: odd}
\forall y:z \neq 0 \And  z \neq ssy
\end{eqnarray}
The intuitive solution of (\ref{eqb: odd}) is $z = s(0)$, \ie 
according to Definition~\ref{def:sost-as-sol} the substitution 
$[s(0)/z]$.  We will use the rules in Figure~\ref{fig:fo-disunif} and 
gloss over normalization steps as elimination of trivial 
(dis)equations .  Branches stemming from the explosion rule are 
numbered and pursued separately (keeping in mind that they form a 
disjunction, \ie a finitely branching tree from a search standpoint).  
$R(x)$ denote application of the rule $R$ on variable $x$.  Sometimes 
we use the more informative notation $R(s=t)$.

\begin{Example}
\label{ex:num}
\[ \begin{array} {ll}
\fbox{$\forall y: z \neq 0 \And z \neq ssy$}\\
\Lmap_{E(z)(1,2)}\\
& (1) \ \forall y: z \neq 0 \And z \neq ssy \And z=0\\
\Lmap_{M1(z)}\\
& \forall y: 0 \neq 0 \And 0 \neq ssy \And z=0\\
\Lmap ^*_{Clh(F)} \fbox{$\bot$}\\
& (2) \ \exists x \forall y: z \neq 0 \And z \neq ssy \And z=sx\\
\Lmap_{M1(z)}\\
& \exists x   \forall y: sx \neq 0 \And sx \neq ssy \And z=sx\\
\Lmap^*_{Dec,Clh(T)}\\
& \exists x \forall y: x \neq sy \And z=sx\\
\Lmap_{E(x)(2.1,2.2)}\\
&(2.1) \ \exists  x \forall y: x \neq sy \And z=sx 
\And x =0\\
\Lmap_{M1(z)}\\
&  \exists  x \forall y: 0 \neq sy \And z=s(0) 
\And x =0\\
\Lmap^*_{Clh(T)} \fbox{$z=s(0)$}\\
& (2.2)  \ \exists x_1 x \forall y: x \neq sy \And z=sx \And x 
=sx_1 \\
\Lmap^*_{M1(x),Dec1} \\
& \exists x_1 x \forall y: x_{1} \neq y \And z=sx \And x 
=sx_1 \\
\Lmap^*_{UE_1(y)}  \fbox{$\bot$}
\end{array} \]
\end{Example}


Note that disunification overcomes the difference between {\em linear}
and {\em non-linear\/} terms in the difference between various solved
forms, namely {\em unification} solved form versus a solved form with
constraints \cite{Com91}.
This may ne interprerted as  evidence of the opportunity of rephrasing 
unrestricted relative complements as disunification problems. We on
the other hand maintan that this approach is unncessarly general \wrt
(relative) complement problems. Implementing disunification entails
managing the non-deterministic application of a
few dozen rules which eventually turns a given problem into a solved form.
Though a reduction to a significant subset of the disunification rules
as the one depicted in Figure \ref{fig:fo-disunif}is
likely to be attainable for complement problems, control is a major problem.
We argue that using disunification for this purpose is unnecessarily
general.  Moreover the \ho case results in additional complications, such as
restrictions on the occurrences of bound variables, which fall outside an
otherwise clean framework.  As we show in this dissertation, this must not
necessarily be the case.  We believe that our techniques can also be applied
to analyze disunification, although we have not investigated this
possibility at present.

% On the other hand, absorbing complements inside 
% disunification offers a neat gain in term of elegance, declaratively, 
% generalizability both to various type-theory and to more complicated 
% syntax.  In summary it inherits all the advantages of a sound and fast 
% developing subfield in equational studies. 

