\section{Classical Negation}

It is a basic fact of classical first-order logic that propositional 
connectives are inter-definable; more precisely some subsets of all 
operators provides by definition the missing ones; this is an immediate 
consequence of their truth-value semantics.  It is therefore customary 
and convenient --- to save cases in structural inductions --- to 
assume as primitive only some operators and define the others in terms 
of former with the proviso that they form a complete basis.  In almost 
every definition negation is taken as primitive, paired either with 
conjunction, disjunction or implication; even those more succint
presentations based on a singleton connective as {\em nand {\rm or} 
nor} retain an implicit flavor of negation.  The same remark applies 
to a notion of negation defined via a propositional constant for 
falsehood. This provably goes back to Kolmogorov and it is 
motivated by what Girard \ref{Gir91} likes to call the Heyting 
semantics.  

There is yet another way to address negation which is peculiar to 
classical negation and is related to the transformational approach we 
are interested in.  This is known as {\em negation normal form} and it 
is used for example in Tait's concise proof of cut-elimination for 
classical logic \ref{Sch77}.  For every atomic predicate symbol $p$ we 
also have a symbol denoting the opposite, say $\ol{p}$.  Then, with 
the essential usage of double negation elimination and De Morgan' s 
laws, negation is introduced as expected:

\[
\neg p =_{def} \ol{p} \quad\quad \neg \ol{p} =_{def} p \quad\quad 
\neg \neg p =_{def} p \]
\[
\neg (A \And B) =_{def} \neg A \Or \neg B \quad\quad \neg (A \Or B) 
=_{def} \neg 
A \And \neg B
\]

Thus, as far as the classical propositional structure is concerned, 
negation can be achieved by renaming. Consistency is then achieved by 
adding axioms that specifies that is it inconsistent to hold both $p$ 
and $\ol{p}$, \ie something like $p \Bimp \neg \ol{p}$.

\subsection{Renaming to Horn format}

For accident or necessity (though now we lean for the former)
Horn logic imposed itself as {\em the} format in logic programming.
Though Turing-complete etc...

% Rather than extending the syntax in an ad hoc way or introducing
% dubious operators as \NF, 
A first possibility to be attempted is to
investigate how far we can go by renaming to Horn format, 
especially as negation is concerned. 

%\subsection{Renaming algorithm}

Informally, the reasons why this is feasible is classical and 
intuitionistic logic coincide as far as the Horn format is concerned. 
Several straightforward proof-theoretical arguments are known 
\ref{??}. This yield that classical equivalences  
preserve the intended operational semantic of the source program.


%%%%%%
\subsection{What is failure}

Discussion on whether complementation is to be performed only on 
decision procedures or also on possibly non-terminating programs, 
r.e. predicates (like demo). What is the failure set of demo? 

























