%Contiene:  1. satogen 2. SH CET 3. SH CET mia 4. Cng per predicati
% Frank comments on Comon rules 5
% 6 DNF vs CNF and solved form with constraint



% %%%%%% satogen

At this point we present the procedure in its generality: the 
following elements have to be taken into account:
\bit
\item
predicates defines by $n$-clauses
\item
$k(i)$ literals in their $i$-th clause
\item
clauses without body.
\enit



\[
\begin{array}{ll}

\forall \xn (p(\xn) \Bimp 
\BOr\limits^m_{i=1}
 \exists \vy (\BAnd\limits^n_{j = 1} x_j=t_{i,j} \And
\BAnd\limits^{k(i)}_{j=1} L_{i,j})
\\
\Lmap_{cp}\\
\forall \xn (\neg p(\xn) \Bimp 
\BAnd\limits^m_{i=1}
 \forall \vy (\BOr\limits^n_{j = 1} x_j \neq t_{i,j} \Or
\bigvee\limits^{k(i)}_{j=1} \neg L_{i,j})
\\
\Lmap_{lift}\\
\forall \xn (\neg p(\xn) \Bimp 
\BAnd\limits^m_{i=1}
(\forall \vy (\BOr\limits^n_{j = 1} x_j \neq t_{i,j}) \Or
\bigvee\limits^{k(i)}_{j=1} \exists \vy (\BAnd\limits^n_{j = 1} x_j = 
t_{i,j} \And \neg L_{i,j}))
\\
\Lmap_{dnf}\\
\forall \xn (\neg p(\xn) \Bimp 
...
\\
\Lmap_{disunify}\\
\forall \xn (\neg p(\xn) \Bimp 
...
\\
\Lmap_{prettyp}\
...
\end{array}
\]


%%%%%%%%%%% Nornal form: added




The following %%%%%%%%% SH CET

\[
\begin{array}{llr}
 \frac{} {\prv t\equiv t} {\small{(\prv\equiv)}}
& \frac{\Gamma \prv G}{\Gamma, x\equiv x \prv G}{\small{(\equiv 
\prv})}\\
\mbox{} & \mbox{} & \mbox{}\\
\frac{[t/x]\Gamma \prv [t/x] G}{x \equiv t, \Gamma \prv 
G}{\small{(Leib-L)}}
&
\frac{[t/x]\Gamma ]\prv [t/x] G}{t \equiv x, \Gamma \prv G}{{Leib-R}} 
& \mbox{provided $x$ does not occur in $t$}\\
\mbox{} & \mbox{} & \mbox{}\\
& \frac{} {f(\tn) \nq g(\sm)) , \Gamma \prv G}{Clh}  &\mbox{for 
distinct }  f,g \in \Sigma \\
\mbox{} & \mbox{} & \mbox{}\\

\frac{} {x \equiv t[x]) \Gamma \prv G}{ Occ} 
&
\frac{} {t[x] \equiv x) \Gamma \prv G}{Occ} & \mbox{if $x$  occurs  
properly  in $t$} \\
\mbox{} & \mbox{} & \mbox{}\\

 &
 \frac{\tn \equiv  \tn^\prime, \Gamma \prv A}{f(\tn) \equiv 
f(\ol{\sm})  } \Gamma \prv A) & \mbox{for all }   f \in \Sigma\\
\end{array}
\]

%%%%%%%%%%%%%% 3. SH CET mia %%%%%%%

\newcommand{\eqp}[2] 
{#1 \stackrel {\textstyle \cdot}{\equiv} #2}

 Note that we stipulate to look at 's=t' as the multiset composed by 
$s$ and $t$: then $ \eqp s t$  stands ambiguously for for $s = t$ or 
$t=s$  and this convention allows to simplify the transformation 
rules dropping the exchange rule, as in \cite{Sny91}. We can then 
reduce the SH rule-set

\[
\begin{array}{llr}
 \frac{} {\prv \eqp t t} {\small{(\prv\eqb)}}
& \frac{\Gamma \prv G}{\Gamma, \eqp x x \prv G}{\small{(\eqb \prv})}\\
\mbox{} & \mbox{} & \mbox{}\\
&
\frac{[t/x]\Gamma ]\prv [t/x] G}{ \eqb t x, \Gamma \prv G}{{Repl}} & 
\mbox{provided $x$ does not occur in $t$}\\
\mbox{} & \mbox{} & \mbox{}\\
& \frac{} {f(\tn) \nq g(\sm)) , \Gamma \prv G}{Clh}  &\mbox{for 
distinct }  f,g \in \Sigma \\
\mbox{} & \mbox{} & \mbox{}\\

&
\frac{} { \eqb x t[x]) \Gamma \prv G}{Occ} & \mbox{if $x$  occurs  
properly  in $t$} \\
\mbox{} & \mbox{} & \mbox{}\\

 &
 \frac{ \eqb  \tn\sn \Gamma \prv A}{f(\tn) \eqb f(\sm)  } \Gamma \prv 
A) & \mbox{for all }   f \in \Sigma\\
\end{array}
\]

%%%%%%%%%%% 4 CNG %%%%%%%%%

\[
(Cng): & \forall(\ol{\xn  = \ol{y_n}} \Imp p(\xn) \Bimp p(\ol{y_n}))
 & \mbox {for   all predicates }   p \in \Sigma^p\\

(Cng^w): & \forall(\ol{\xn  = \ol{y_n}} \Imp p(\xn) \Imp p(\ol{y_n}))
 & \mbox {for   all predicates }   p \in \Sigma^p\\
\]

%%%%%%%%% 5 Frank and Comon%%%%%%%%

Note AGAIN THAT OC IS FORMULATED for terms rather than for variables, 
though even the latter formulation when universally quantified 
subsumes clash


EE3 as a sort of axiom of infinity: need to make every disequation 
true so that $d$ is absorbed and you can always make this true by 
introducing a new parameter, given the occurrence proviso

%%%%%%% 6%%%%%
Need to make consistent boolean normal form and the definition of 
soved form: the one in CL goes with cnf? Example: the solution
of nonedge(a,b) is a disjunction of conjunction rules ED may not be 
sufficient ro get into sol with constraints

%%%  7 %%% ADDED
\subsubsection{About Cardinalities}
It seems that  a fair part of the disunification game turns around
the question of  finiteness vs. infiniteness of signatures: this, in a 
typed context, comes in two flavors:
\bit
\item finite vs.\ infinite signatures
\item finitary vs.\ infinitary sorts (types)
\enit

We discussed the first aspect in the beginning of the third chapter. The 
second one is potentially more worrisome. Indeed, a type is called 
\emph{finitary} iff the set of all closed normal forms of this type is 
finite. This situation occurs pretty frequently: think, in a \fo\ 
context to a finite graph, or in dependent types to the normal form 
of a natural deduction derivation. As a matter of fact, the 
many-sorted \fo\ rules for disunification \cite{CL89} have special rules for 
the finitary case, essentially turning an universal quantifiers into a 
finite conjunction of cases. Lugiez \cite{Lug95} assumes all types to 
be infinitary, relying to the kind of explosion we have delineate in the 
latter paragraph to treat the finitary case. It would thus appears 
that we need to different kind of set of rules for the two cases. Now 
it is well-known, that as far as dependent types aree concerned this
diffeterence is undecidable, due to the presence of empty types, like
\[
\exists x: (natded \bot}.\top \Lmaps_{*} \bot
\]
The challenge is thus to show that the finitary rules are 
\emph{admissible}: otherwise the all enterprise have to retreat 
into more safer bounds.

More indetails the quastion is whether the universal finitary tule at 
\ho can be emulated by an iteration of UEXPL, \ie by  recursion on 
the $\l$-term. At \fo\ they are the same. UEXPL trats every case. in 
simple typles HOUEXPL proposes only an initial binding and thus looks 
like it is likely it needed iteration.

State lemma.

In this case, for universal quantifiers, the infinitary rules would 
suffice giving a partial solution to the mentioned decidability 
problem 

To be completed

%%%%%


%%  Add the sort-sensitive rules 

%%%% 8 %%% DONE
\subsubesction{Solving Arbitrary Equationalo Formulae}

Notwithstanding our interest concerns mainly $\Sigma-2$-formulae$, \ie 
equational problem,and the rules are tailored only for the latter ,
 since $CET$ is decidable,  you may wonder how to solve arbitrary 
 equational formulae. The good old nethod is quantifier elimination, 
 as in \cite{Mah88}, but only up to $\Sigma-2$-formulae$. This makes 
 isd pretty simple. Suppose we have a formula $\cP = 
 \vec{Q}\forall\ldots\exists\ldots P$. Then its set of solutions is 
 equal to the complement of the set of solutions of $not(\cP)$. 
 Iterate this procedure and you get a prenex (or the negation) of an 
 equational problen which can be solved by disunification. Rather 
 than detailing the procedure we show how to solve into $\top$
the $DCA(nat)$. We will pretty informal.
\[
 \forall y. y=0 \Or\exists x. y=s(x) \Lmaps_{\rm prenex} 
 \forall y \exists x: y=0 \Or  y=s(x) \Lmaps^{*}_{E,Dec} \Top
\]


%%%%%%%
def (dis)equation, trivial




make precise notion of solution as in CL (AWAY)

From an algebra to rewrite rules

check p 393 cl 

control: solved parameter p 395

%  CL claim that in cnf you need only assoc and comm of \And and \Or: 
% p377  DONE
