\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 extreme 
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\footnote{This provably goes back to Kolmogorov and it is 
motivated by what Girard \ref{Gir91} likes to call the Heyting 
semantics.  We will have more to say in the next chapter.}.

There is yet another way to define 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? 


