\documentstyle{book}
\include{tcom}
\begin{document}

\chapter{Introduction}
\section{Overview}
\section{Preliminaries}
Definitions and conventions, two words on \lp and transformation on 
them
\section{Motivations}
\subsection{\ho \lp}
Taken from Nadathur \& Miller survey
\subsection{Elf}
From Frank`s book

\chapter{What is Negation}
A cursory look to the formulation of classical and constructive 
negation, possibly using Gabbay and something from Curry`s textbook.
\section{Minimal Negation}
\section{Intuitionistic Negation}
\subsection{Negation as inconsistency}
Gabbay
\subsection{Structured Negation as inconsistency}
Gabbay \& Wansing
\section{Intermediate logics}
How negation behaves in constructive systems between Int and C
(Ornaghi-Miglioli)
\subsection{strong negation}
(Nelson-Wansing)
\section{CLASSICAL NEGATION}
\section{NF}

Dickhoff and Harland unprovability sequent system

\subsection{Formulation in Analytical Calculi}
A common way to look to sequents is as a proof-search formulation of 
natural deduction; yet this may enforce some choices (as singleton 
conclusion) that appears to be limiting for a in-depth analysis of 
the role of negation.
\subsubsection{Intuitionistic PC (IPC)}

They come in two flavors: sequents (Gentzen) and tableaux (Beth, 
$ST$), 
coming respectively from a syntactic and semantic standpoint.
Consider positive IPC (no negation even defined, no absurdity).
Add negation to sequents ($SQ$); options:
\begin{itemize}
\item
$SQ^\perp$ negation defined and DSL rule: 
\item
$SQ^\neg$ negation primitive:
\item
parametric negation (Frank-Kleene) and DSL rule: 
\item
negation with certain falsum (Miglioli-Ornaghi)
\end{itemize}
\subsubsection{On Duplication}
Not\footnote{may be skipped as irrelevant} all duplications are the 
same: as far as IPC can go two ways: $LJ \Rightarrow LJT $ or $ST 
\Rightarrow  ST^{F_c} \Rightarrow ST^{F_c}T$ (T for terminating).
\subsubsection{NF as unprovability}
\chapter{Negation in logic Programming}
From my master thesis
\section{Overview of /\nf  in /\lp}

\subsection{Constructive negation}
Chan-Stuckey-Drabent: the constraint \lp \ approach, in the 
likelyhood that we have constraints as a residue of the transformation
\section{Negation and Uniform Proofs}
From Frank`s notes on ATP and some paper of mine

\subsection{NF, \lp and termination}
From Frank \& Ekk.\ paper on  modes and Bol`s thesis: when a
logic program is a decision procedure; finite and infinite failure, 
negation of r.e. logic programs

\chapter{The state of the art on the transformation}

This will be the final stage of the document I gave you
\section{Complement Problems} 
\section{Background on fo-(dis)unification}
\section{Equational Problems and Disunification}
\section{Putting it together}
\section{The Trouble with Local Variables}
\section{Logic Programming and Universal Quantification}
\subsection{Covering}
\subsection{More on DCA}
\subsection{The CASE algorithm}


% \chapter{First-Order Extensions}
% \section{Motivations}
% On the necessity of hypothetical and parametric judgments in logical 
% frameworks
% \section{Embedded Implication}
% \label{imp}
% 
% Is there an obvious extension of the transformational approach  ? 
% Completion of Nprolog programs\footnote{find a better example}: 
% difference between classical and intuitionistic logic
% in the manipulation of the completion: do we have to use Pedreschi @ 
% operator as below?
% 
% \begin{Example}\[\begin{array} {l}
% horn (all(C)) \leftarrow \forall x. (term(x) \supset horn (C \ x)).\\
% horn(imp(G, A)) \leftarrow  atom(A), conjunction (G)\\
% horn(A) \leftarrow atom(A).\\
% \end{array} \]
% 
% \[\begin{array} {l}
% nonhorn (all (C)) \leftarrow \forall x. (term(x) \supset nonhorn (C \ 
% x)).\\
% nonhorn(imp  (G, A)) \leftarrow  nonatom(A); nonconjunction (G)\\
% nonhorn(and (A ,B)) \leftarrow nonatom(and (A, B)).\\
% \end{array} \]
% 
% \end{Example}
% 
% Unfortunately, this does not seem to be general enough, perhaps 
% depending on the difference between predicates under the Closed vs.\ 
% Open World Assumption. Namely, predicates occurring negatively
% in an implication are taken to be open, since they are going to 
% dynamically join the program and thus cannot be completed \`{a} la
% Clark. In the former example ``term'' is such a predicate. This seems
% to rule out {\em non-hypothetically stratified} implications. Hence:
% 
%  \subsection{Elimination of implication}
% \begin{Example}
% 
% \beq
% trivial(imp(A,  B)) \leftarrow trivial(A) \supset trivial(B)
% \eneq
% 
% One idea is to efficiently keep explicit assumptions:
% \[\begin{array} {l}
% trivial(imp(A,  B)) \leftarrow  trivial2(A,B)\\
% trivial2(A,A).\\
% trivial2(C,A \Imp B) \leftarrow trivial2(C,B);trivial2(A,B).
% \end{array} \]
% \end{Example}
% 
% A technique to eliminate implications passing through a $S4$-modal 
% prolog and back to horn clauses is described in Giordano\& Martelli 
% paper in ELP96.
% 
% \section{Generic Goals}
% What about parametricity? It seems that intensional
% quantification is preserved under the negative transformation,
% (see the ``horn'' example)
% though one would have to keep track of the extension
% of the signature. There is an obvious  tension between
% OWA and CWA (in the sense of having CET or CET and DCA) that could 
% turn out to be problematic.
% Hopefully, we shall use CASE for $\forall^e$
% and the GENERIC operation for $\forall^i$. 
% 
% Total darkness at this time for LF $\Pi$ operator.

\chapter{HO-Extensions}
\section{\ho horn logic}
Two sides:
\bit
\item `Functional` \lp
% Trouble may start for clauses with \ho predicates
% in extensional position---say the
% transitive closure example or {\tt mappred}. It seems difficult to 
% transform at compile time a predicate variable:
% \bit
% \item conservatory solution: $R$ can be only atomically instantiated: 
% use DCA to unfold it (actually just a first-order schema)
% \item no restriction; execute at  runtime with Nelson negation,
% with all the problems that such an extension causes (conservativity, 
% tractability)
% \enit
\item $\l$-terms as data structure (\ho abstract syntax): 
\enit

Distinguish the two langages

\subsection{HH- without predicate quantifications}
\subsection{Pattern Disunification and Transformation}
Hopefully improving on Lugiez algorithm
% \subsection{LLambda}
% Putting it together; the transformation for LLambda
\subsection{Beyond Pattern for HH-}
Have some  experimental evidence of the behavior (termination, 
residues) of disunification for typical programs
\subsection{HH with predicate quantification}
% \section{$\l$-Prolog}
% Putting it together; the transformation for hohf, or a decent fragment
\section{Ur-ELF} a higher-order language extending HH- with 
$\all,\Pi$, but essentially first-order as quantification is 
concerned and not type-theoretic: Thru the l-cube get to

\section{ELF}
% Big question mark: with how little effort will the thing do for Elf
\section{CC}

\appendix
\section{Appendix: Regular Splitting}
Taken from my paper(s) with Mario; presenting an alternative, 
proof-theoretic transformation technique.
\end{document}

