\section{Extending Horn Logic}

As previously mentioned, once Horn logic was isolated as the core of a 
programming language, a fairly disorderly race was off to get more 
mileage out of Prolog. % This endorsed a failure to consider the two 
% facets of this new style: that not only logic was a powerful programming 
% language, but maybe more importantly that programming can be imbued 
% into logic. While supporters of the first point would go out without 
% lasting results, only the latter, we contend, hit the target.
%
 To sum up, we can isolate several (slightly overlapping) 
positions:

\begin{itemize}
\item The ``tories'': for model-theoretic reasons, Horn logic is the
  best possible world, see the manifest ``Why Horn logic matters in
  computer science" \cite{Mak87}.
\item The ``realists'', guided by Apt: \lp \emph{is} Horn logic with
  \nf: what's left to do is logicize the impure features of Prolog.
\item The ``Making Prolog more expressive'' people:
%        to be pedantic, this ought to be 
  divided in two main intertwined sub-tribes: the ``logicians", which
  claim that programming in Horn logic is like living with one hand
  tied behind your back, and the ``compilers" (see Sato and Tamaki.
  \cite{Tamaki84}: those come from the specification approach and look
  at Horn logic as a implementation language which is the target of a
  long and tiresome travel through derivation and/or transformations from
  \fo logic.  For the logicians, it is a must to conquer any piece of
  land outside Horn logic, say by adding connectives \cite{Poole85},
  pre-compilation \cite{Lloyd84}, change of interpreters (say
  connection graphs~\cite{Gallier87}) or, more reasonably, switching from
  classical logic to fragments in the intuitionistic galaxy, reviewed
  in Section~\ref{sec:lamrelated}.
        
\item Finally, there is the proof-theoretic approach of uniform
  proofs: new connectives are allowed only if we can ascribe a clear
  meaning in term of search and provide a way of endowing \lp in a
  purely logical way with features such as modules, data abstraction and
  scoping typical of other mature languages.

\end{itemize}

We now concentrate on how recent research has tried to address some
of the problems connected with \emph{NF}.

\subsection{Constructive Negation}
\label{sec:cn-gen}
{\em Constructive Negation} is an attempt to devise methods capable to 
provide logically justified answers to non-ground negative queries, in 
analogy with the witnessing property of constructive logics.  Formally, for a suitable derivability relation, this 
property ensures that from $ \prv 
\exists x \Not p(x)$ we can  infer the existence of  a term $t$ such that  $ \prv 
\Not p(t)$.  We can roughly distinguish two approaches:
\begin{itemize}
\item[i.]
Program Transformation: \cite{Sato84}, \cite{Foo88}, \cite{Bar90}.
\item[ii.]
Negation by Constraints: \cite{Wallace87} for Datalog programs, 
\cite{Chan88} \cite{Chan89} and extended to CLP in \cite{Stuckey95}; Fail 
Substitutions: \cite{Shepherdson89} \cite{Mal89}.
\end{itemize}


Historically, the original attempt to deal with the issue was simply to 
try avoiding the floundering phenomenon: given that the latter is in 
general undecidable, one possibility is to try to make sure that when 
a negative literal is called it has already been grounded: there are 
basically three possibilities:

\begin{enumerate}
\item
 Satisfy the syntactic, though very restrictive, conditions on 
 allowed computations \cite{Shepherdson85}, which essentially reduces 
 evaluation to {\em ground} evaluation.
\item
Try to achieve grounding by delaying as in {\em [M]NU-Prolog}
\cite{Naish86} or {\em 
Sicstus} \cite{sics}, where a goal may be declared to be ``frozen'' and is 
evaluated only when it reaches a sufficient degree of instantiation.  
This is obviously only a partial solution, since at run-time there is 
no guarantee to eventually ground the problematic query.  A more
complex and historically less successful alternative
 is offered by the computation rules of {\em IC-Prolog}, which allow
 the computation of negative open queries if their positive
 counterpart does not bound any variable 
(see \cite{Naish86}, for a comprehensive analysis and references).
\item
Covering the open negative query with a generator of values for the 
relevant variables. This is further detailed next.
\end{enumerate}

\subsubsection{Static Approaches}
\label{stat-rel}

If we are dealing with Datalog programs, i.e.\ with finite Herbrand 
Universe ($U_P$), the naive approach would be to instantiate all the 
rules with potentially troublesome goal with terms from $U_P$ 
\cite{Apt88}, say through propagation in every negative literal in the 
program.  This is clearly infeasible, since it may result in an 
intractable numbers of rules, especially in an untyped setting.

A sophistication of this idea can be found in \cite{Foo88}: the 
proposal is to automatically infer a `type' for the problematic 
variables and transform the original program into one where grounding 
is ensured by coverage from those types.  Then useless answers 
originating from general instantiation would be excluded by the typing 
discipline.  Although it can be shown that the new program is 
equivalent to the old one, this cannot be extended to full Prolog: 
function symbols make the type infinite and non-ground facts would 
undermine the instantiation capability of the type. 

Finally, the transformation approach falls in this category and is
detailed in Chapter \ref{ch:hornelim}.

\subsubsection{Dynamic Approaches}

Chan \cite{Chan88} is acknowledged to be the inventor of the term 
'constructive' negation in this area; his approach can be roughly characterized as 
 mixing  {\em NF} with a constraints-solving attitude.  In essence it 
consists in evaluating a negative goal by executing its positive version and 
by negating the answer obtained.  As in the \emph{CLP} family of languages, 
unification and disunification are kept explicit and returned as 
solutions.    Of course, we need to keep 
the (in)equalities in normal form and there are some 
obvious problems when dealing with computations that have infinite 
answers; those are  addressed in a following paper (\cite{Chan89}),
by quantifying over the answer 
substitutions.  No proof of completeness is offered. 
We can offer the following  rational reconstruction: the key observation is 
that if $G$ is a goal and we consider the answer substitutions 
$\q_1,..., \q_n$ as  equations, $G \Bimp \exists(\q_1 \Or 
\dots \Or \q_n)$ is a logical consequence of the completed database.  
Therefore the constructive negation rule is simply $\Not G \Bimp \Not 
\forall(\q_1 \Or \dots \Or \q_n)$, where the right-hand side can be 
simplified by disunification. For instance given the query $
not(even(X))$, its positive version yields the answer $ 
X=0\Or \exists Y : X= s(s(Y))$, whose negation is  $X\nq 0\And \forall Y: X \nq s(s(Y))$: its solved form 
is hence $X=s(0)$, which we can regard as a more informative 
refinement of the answer constructive negation produces.

 A generalization 
to constraint logic programming over arbitrary structures is given
in \cite{Stuckey95}; it turns out to be sound and complete w.r.t.  the 
three-valued models of the completion. Other development of 
constructive negation are addressed in \cite{Fages97}.

\smallskip $(E)SLDNF-S$ (\cite{Shepherdson89}) The finite failure case
in the definition of $SLDNF$-resolution is modified as follows: a goal
$(\Gamma, \Not A)$ has a descendent $\q\Gamma$, if there is a finitely
failed-tree for $\q A$, where $dom( \q ) \in FV(A)$.  So {\em NF} can
instantiate under success, i.e.\ negative goals may directly return
substitutions: given $P$ and $G$ the aim is to look for a (fail)
substitution $\q$ such that $P \vd\q G $ has a finitely failed tree;
then by the soundness of the {\em NF} rule $\forall \q \Not G$ is a
consequence of $comp(P)$ and thus $\q$ is an answer substitution for
the query $\Not G$.  This seems very costly, since it entails
enumerating (guessing) every fail substitution. I am not aware of any
implementation of this proposal.

This is refined in \cite{Mal89}, where it is shown how to avoid to 
generate all possible substitutions in lieu of a maximal general fail 
substitution.  Moreover, the improvement \wrt Chan's work lies in 
the feature of always including some positive bindings for the 
variable in the negated goal.  If the $SLD$-tree is infinite, the 
method  enumerates the set of 
fail substitutions; this corresponds to the fact that in general 
negative queries cannot be represented by finite positive information 
alone (connected to \cite{Lassez87}).  
% Note anyway that $(E)SLDNF-S$ 
% turns out to be complete for a three-valued possible world semantics 
% of $comp(P)$.

\subsection{Non-Failure Driven Negation}
\label{nfs-neg}

During the years ways of incorporating other more logical forms of
negation than NF have appeared.  Since most of the time this gives
back full non clausal-logic, most of them are cataloged as automated
theorem provers.  In all these accounts, negative information has to
be provided explicitly and specific rules are offered to deal with
that.  Sometimes it is possible to mix ``open world'' and ``closed
world'' predicates safely.  For a more detailed account and
bibliography, let me refer to \cite{Momigliano92}.
\begin{itemize}
\item {\em N(Q)Prolog} \cite{Gabbay84}, a complete implementation of
  positive intuitionistic logic.  By defining disjunction classically
  and allowing a restart rule (see \emph{nH Prolog} next), Gabbay
  shows it to be complete for full classical logic as well.
  
\item {\em Negation as Inconsistency} (\cite{Gabbay86}). Here we
  evaluate a query against an ordered pair $ \la P,N \ra $, where $P$
  is a Horn program and $N$ a set of queries that are required {\em
    not} to succeed; this is logically equivalent to adding to the
  program the negation of all the members of $N$, and permits
  importing negative facts and rules.  Both systems have a very
  awkward first-order version.
  
\item Stickel's \emph{PTTP}, supplements \SLD-resolution with the
  model elimination rule.  This entails keeping track of the ancestors
  of the goal, loosing one of the key feature of Prolog, namely input
  resolution.

\item
Loveland's \emph{nH Prolog} \cite{Reed92} incorporates case analysis in \SLD-resolution,
by demanding the invocation of a restart rule for every disjunctive
head, until the stack of the former.  Without requiring 
contrapositives (as in \emph{PTTP}), it simulates case analysis with different runs of 
essentially the Prolog engine.  Unfortunately naive \emph{nH-Prolog} is 
incomplete and the new versions (\emph{Progressive nH} and \emph{Inheritance nH}) 
have a less natural and convincing description.

% \item
% Plaisted \cite{Pla88} instead is concerned with a difficult attempt to 
% use sequent-based logic programming with a version of the cut rule 
% which operates backwards leading to a problematic guessing of its 
% premises.  For a comparison, see 

\item
Another extension goes under the name of {\em disjunctive logic 
programming} (see \cite{Lobo91} and references therein).  It aims to 
deal with full clausal logic by generalizing  Horn clauses to
disjunctive heads.  
% In particular the procedural semantic, called 
% $SLO$-resolution, extends the $SLD$-step by having the selection 
% function choose a clause in the current goal (a sequence of clauses) 
% and trying to find a clause whose head subsumes it; if successful, the 
% goal is incremented by the body, without deleting the selected clause.
\end{itemize}

\subsection{Proof-Theoretic Approaches to Negation and {\em NF}}
\label{pt-rel}

In the 90's there has been  an attempt to tie LP to proof-theory, 
where it belongs: and this has brought new insights, particularly on 
{\em NF}.

The first step is to view Horn clauses positively as rules and goals
as existentially closed conjunctions of atoms to be proved by the
former.  Historically this can probably be dated back to Gabbay and
Reyle \cite{Gabbay84}.  It is customary \cite{Halnass90} to
distinguish among two approaches:
\begin{itemize}
\item[1.]
Clauses as axioms (programs as theories) and some form of Gentzen 
sequent calculus to infer goals, \ie uniform proofs systems.

\item [2.]  Clauses as rules \cite{Halnass90}: Horn (and beyond) programs 
should be seen as set of inference rules for the derivation of (not 
necessarily ground) atoms.  
\end{itemize}

This has the following relation with negation:
\begin{itemize}
\item[1.]  Minimal, intuitionistic and classical negation can be
  superimposed over uniform proofs \cite{Miller89jlp},
  \cite{Harland91iclp}, \cite{Momigliano92}: Minimal negation, being
  camouflaged implication, is executed through the \\
$AUGMENT/backchain$
  operation; the evaluation of $ \Not D$ consists in the assumption
  of $D$ and in the attempt to prove $\perp$ from the enlarged theory.
  The Duns Scoto Law and Reductio ad Absurdum for atoms formalize the
  latter, preserving the feature of abstract logic programming
  languages \cite{Miller91apal}.
\item[2.]  GCLA \cite{Aronson91} is based on the rule-based
  definitional approach to logic programming: it has intuitionistic negation
  built-in, applying the \emph{definiens} operator to the
  left-hand side of a sequent. A discussion can be found in Section
  \ref{gcla}.
\end{itemize}

St\"{a}rk \cite{Staerk92} has given a sequent calculus reconstruction
of \nf using Clark's equality and freeness axioms, negation (switch)
rule and cut rules.  Much more is however contained in St\"{a}rk's
thesis and subsequent research, although not directly applicable to
our goals; to quote a few, he shows that a sequent is provable in this
calculus iff it is true in all 3-valued model of the completion.
Furthermore a completeness result is proved w.r.t $SLDNF$-resolution
for program satisfying the cut-property.



%\subsection{On substrucural logic and \NF}

% Harland \cite{Har92} instead proposes a sequent calculus based on 
% intuitionistic logic that directly incorporates {\em NF} without 
% referring to the completion.  The usual rules, restricted to deal with 
% Horn logic, induce a {\em positive} derivability relation; 
% furthermore, he introduces a {\em negative} system of {\em 
% dis-provability}, denoted by much like $\nprv$ in Figure \ref{fig:sf}
% The 
% two systems are interlinked by the rules for {\em NF}.
% \[
% \ianc{\Gamma \prv^- F}{\Gamma \prv \Not F}{\Not-R+}
% \qquad
% \ianc{\Gamma \prv F}{\Gamma \prv^- \Not F}{\Not-R-}
% \]
% Structural rules have a paramount importance in this calculus: due to 
% the non-monotonic nature of {\em NF}, weakening in the positive 
% fragment is \emph{cautious}, introducing only already provable formulae on 
% the left, resulting in a dual to contraction.  In the negative system 
% structural rules, cut included, are not eliminable.  This is not 
% strictly a calculus of {\em finite} failure, since sequents of the 
% form $p\leftarrow p \nprv p$ are provable, although with the 
% essential use of weakening.  Of course, due to the recursion-theoretic 
% complexity of unprovability, every such an axiomatic formulation is 
% bound to be incomplete.  Moreover the boundary seems fuzzy, as, for 
% example, $p$ is independent from the program $p\leftarrow q, q 
% \leftarrow p$.  The calculus without structural rules is shown 
% \cite{Harland93} to be sound and complete w.r.t.  finite failure and 
% $SLDNF$-resolution (extended to first-order hereditary Harrop 
% formulae).  
% Having to model the operational behavior of {\em NF}, both 
% the positive and the negative system make explicit references to 
% unification, Skolem functions and so forth. 
%  Still, the system is not 
% meant for proof search and requires a relative complement algorithm to 
% provide answers to open negative queries.

% \bit
% \item
% Cerreto's linear formalization of NF
% \item
%%Wansig's strong negation in sub-structural logics
% \enit






