\documentstyle[a4]{article}
\include{com}
\begin{document}

The aim of this thesis is to synthesize the negation of (logic) 
programs in higher-order logic and certain type-theoretic programming 
language as Elf

This is fairly well-known for first-order logic programming, i.e. for 
normal clauses \cite{Bar90} extended to CLP's , even though I find 
the machinery not very appealing

Proceeding bottom-up , the firs thing ids to define a complement 
operation on terms; again an algorithm for first-order terms is given 
in \cite{Bar90}. This is the starting point since we wish to improve 
in several ways, generalizing thru what is will accor as a natural 
hieiarchy

Standard Prolog is not typed: that means that a straightforward Not 
operations will produce alot of irrelevant results (since has ome 
analogy with the proposal in \cite{Foo88}. For example, towards the 
synthesis of the non-member operations on list of numerals
the result of $Not(0)$ contains not only $s(X)$ as expected, but also 
$nil, cons(0,nil) \ldots$. This is going to increase exponentially 
with the size of the signature (not to mention problems with 
modules). Just a simple-type discipline would obliviate this riddle.

\begin{Def}
Let $C$ be a Church simple typing and $\Sigma$ a finitary signature. 
We define $Not(t^\tau)$ by structural induction:
\begin{eqn)
Not(x^\tau) = \empty
....
\end{eqn}

\begin{Example}
$\Sigma = \{0,nil,cons,member\}$
\end{Example}

An alternative characterization can be given by looking at the 
lattice of (fo) terms as originally investigated by \cite{Rey70} 
and \cite{Plo70}. The subsunption ordering induces a poset that can 
be organized in a lattice by seeing glb as unification and lub as 
antinification. A bottom element represents failed unifications, 
while (under quotient after $\alpha$-conversion) (the equivalence 
class of) variables are the top. Every (open ) term standing for the 
set of its instances the former lattice is embeddable in the lattice
of sets of ground terms ordered under inclusion.

Since the notion of complements in arbitrary lattice is well-defined, 
it would be nice to correlate the two characterization,
namely showing:
\begin{equation}
Not(t) = \{t_1, \ldots, t_n \} \Bimp \forall i. t_i^' = t
\end{equation}

Unfortunately this in not immediately achievable since the fo terms 
lattice is not nice: antiunification does not correspond to
set-theoretic union; complement not being unique, distributivity
and modularity are lost. Hence the complement operation has to
be splitted in and-c (pseudo-complement) and or-c, as in 
\cite{Rai58}

\begin{Def}

\end{Def}

\begin{EXample}
SO V SSX  not = Top
\end{Example}

\begin{Theorem
Not(t) = \{t_1, \ldots, t_n \} \Bimp \forall i. t_i^' = t

\end{Theorem)




\end{document}
