\section{From Theorem Proving to Prolog}
\label{sec:history}

A legitimate question is to ask is why \lp does not have a primitive 
notion of negation. 
To understand that, we need to say something on how \lp and Prolog
developed.  This enterprise has a rather peculiar parabola; logic
programming owes its (relative) success to the way it limits and
directs generic theorem proving; from then on, ironically, most of the
effort has been to extend its boundaries without falling back onto
full clausal logic.

Automatic theorem proving, or at least the intuition (and the dream),
can be dated back to Leibniz, but become more of a reality in 1965
when Robinson introduced the resolution principle \cite{Robinson65}.
Briefly, it is a proof procedure which proceeds by contradiction,
converting a sentence to clausal form and testing for inconsistency
with a version of Gentzen's cut-rule augmented with unification. Yet,
this approach has been shown to be in general in-practical.  A great
deal of research developed after Robinson's breakthrough aimed at
restricting the search space, while preserving completeness.  This is
not the place to give even a short account of these studies: we just
sketch those that led to the basis of Prolog as we know it; for
references and a chronology see \cite{Apt90}.  When building a
refutation there are basically two sources of choice:
\begin{enumerate}
  \item Deciding which clauses to pick as parent clauses.
  \item Deciding which literals in those clauses are to be resolved
    away.
\end{enumerate}
One way to support the first restriction is linear resolution,
independently proposed by Loveland and Luckam in 1970, which by fixing
one goal at each step, never needs to resolve two input clauses
together.  As far as the second point is concerned, we may decide,
after Hill, Kowalski and Kuehner, to fix the literal to resolve in the
center clause ('linear resolution with selection function').  Though
we have narrowed the search space considerably, there is still a fair
amount of choice, namely conjunctive choice in the side clauses,
ancestors tracking and factoring.  The winning strategy is to restrict
the syntax of the clauses themselves; the choice fell on Horn clauses:
definite clauses (that is clauses with exactly one positive literal) 
are interpreted as input ones, while Horn clauses with empty positive
part are taken as goals.  Eventually we have arrived at pure Prolog or
\SLD-resolution.

What has \SLD-resolution to do with programming?  The answer can be 
found in the so-called procedural interpretation of Horn logic.  
Although the origins of Prolog are shrouded in mystery, it is known 
that in 1972 both Kowalski and Colmerauer came up with the idea that 
(a subset of) logic could be used as a programming language.  A 
definite clause $A \leftarrow B_{ 1},B_{ 2}, \dots ,B_{ n}$ can be 
viewed as a definition of an Algol-like procedure: 
\pagebreak
\beq \textbf{procedure} \; A 
\\
\textbf{begin}\\
 & call\ B_1 \\
 & call\ B_2 \\
 &  \vdots \\
 & call\ B_n\\
  \textbf{end} 
\eneq 
Goal invocation corresponds to procedure invocation, and the 
ordering of the goals in the body of the invoked clause corresponds to 
sequencing of statements.  In logic programs data manipulation is 
entirely achieved by means of unification, which encompasses parameter 
passing, multiple assignment, record allocation, data construction and 
selection.
 

In spite of its limits, it can be shown that Horn logic has the same
computational power of every other programming language \cite{Apt90}.
Moreover, Horn logic has some nice model-theoretic properties, namely
the minimum model property; it is natural to consider the latter as
the declarative meaning or the intended interpretation of a program.
Therefore it has been argued that we should be content with Horn
logic, which seems to be a complete and reasonably efficient
computational logic.  However, many have been dissatisfied with the difficulty
to express even the easiest logical problems in a language that lacks
(explicit) disjunction and negation. We share this complaint up to a
certain point. We maintain the \lp works as far as the logical and the
algorithmic parts do not differ too much, and that Kowalski's motto
``Programs = Logic $+$ Control'' has shown its intrinsic limitations.
Yet, we strongly share the idea that especially from a programming
point of view it would be advisable to have the possibility of
performing negative queries and overall to have a negation operator in
the body of clauses instead of simulating it with extra-logical
constructions, which make programs less understandable and
declarative.  It is not a question of expressive power, it is a matter
of style and convenience.

There are three ways, in order of increasing complexity, to add
negation to Horn logic:

\begin{itemize}
\item Negative atomic queries.
\item Negative literals in clauses bodies.
\item Negative heads.
\end{itemize}

It is not possible to try to review all the proposed extensions;
historically much of the attention has been concentrated on
incorporating \emph{NF\/}; from that, most of first-order expressivity is
recovered \cite{Lloyd84}.

\section{Negation-as-Failure}
\label{sec:nf}

Since negative information is independent from definite programs, a
specialized inference rule must be invoked: negation as failure
(\emph{NF}), which in logic programming, originated from the
confluence of two quite different trends of research: the refinements
of resolution based automatic proof procedures and the relational
approach to databases.  For a nice introduction see
\cite{Shepherdson88,Apt94}.  The idea of a proof under the \emph{NF}
rule is a natural one: suppose you have a set of axioms and some kind
of inference mechanism which produces a recursively enumerable set of
theorems, and that you are asked to verify the truth of a negative
conjecture $\Not C$ under \emph{NF}; then you try to prove $C$ from
your theory; if you succeed, then $ \Not C$ does not hold, while if
you realize (in a finite time) that $C$ is not provable, then you are
entitled to assert that $ \Not C$ holds.  Its basic idea is to state
that a goal is false if we are able to prove that it cannot be proved
by the program.  Actually, \emph{NF} is more a computational than a
logical notion; we answer `no' to a goal because our attempt to say
`yes' failed, so we say `no' because we cannot say `yes;.  Differently
from other kind of negation, \emph{NF}\\
 ``\dots does not follow from
some constructive knowledge, but from lack of knowledge''
(\cite{Gabbay91elp} pp.\ 8).  That motivates its intrinsic
non-monotonicity: in fact, in dynamic databases every enlargement may
cause the meaning of failure to change and so turn success into
failure.


In logic programming, \emph{NF} works this way: 
\begin{quote}
  " \dots The basic idea is to use \SLD-resolution augmented by the
  \emph{NF} rule.  When a positive literal is selected, we use
  essentially \SLD -derivation to derive a new goal.  However, when a
  ground negative literal is selected, the goal answering process is
  entered recursively in order to try to establish the negative
  subgoal \dots Having selected ground negative literal $ \Not A$ in
  some goal, an attempt is made to construct a finitely failed
  \emph{SLDNF} tree with root $\leftarrow A$ before continuing with
  the remainder of the computation.  If such a tree is constructed,
  then the subgoal $ \Not A$ succeeds.  Otherwise, if a
  \emph{SLDNF}-refutation is found for $ \Not A,$ then the subgoal
  fails \dots " (\cite{Lloyd87} p.\ 87).
\end{quote}

 
The operational nature of this rule motivates the lack of a unique
semantics and some of its related troublesome features: to begin with,
possible unsoundness: without run-time checks on the substitution
returned by a negative open query, the final answer substitution may
not be
 a logical consequence of the program. This is the so-called
``floundering'' phenomenon, the undecidable question of whether the
computation will reach a negative open query and abort. Soundness is
preserved only for ground queries; the flip side of the medal is that
now negation is not a first-class connective, but just a test that
cannot return substitutions. We review in Section \ref{sec:cn-gen} how
and with what computational cost this can be avoided.  And of course,
\NF is in general \emph{incomplete} in general logic programming.

All of the above makes \nf a suspicious candidate for a negation
operator in any \lp language, but the situation is even worse in \lf s.
Even if we manage to isolate a well-behaved logical fragment, such as
acyclic normal programs \cite{Apt90iclp}, %  which exhibit a good
% termination behavior with respect to a large and natural class of
% general goals and for for which completeness \wrt to the most widely
% held semantics holds,
allowing \NF in a \lf\ carries some additional problems. First, the
meta-theory becomes really unwieldy, as both provability and
unprovability must now be taken into account. The 
two systems would be interlinked by  rules such as:
\[
\ianc{\Gamma \nvd F}{\Gamma \prv \Not F}{\Not-R+}
\qquad
\ianc{\Gamma \prv F}{\Gamma \nvd \Not F}{\Not-R-}
\]
where $\nvd$ denotes a proof system for finite failure. In a type-theoretic \lf
this issue is further exacerbated by the need to deliver evidence of
what a proof of a certain judgment is. The most popular way, since the
Automath project \cite{DeBruijn80}, is to to see derivations as lambda
terms inhabiting judgments seen as types. Although it is in principle
possible to associate proof-terms to a derivation by
negation-as-failure -- this is implicit in the denial proof system
that we present in Chapter~\ref{ch:cc}, Figure~\ref{fig:sf} and
\ref{fig:imm} -- the
existence of (unique) canonical forms is in general impossible to
achieve; and this is pretty much a death sentence for \emph{NF}. In fact, in 
% The situation is even further complicated when we step to
frameworks with hypothetical judgments, as recognized first by Gabbay
\cite{Gabbay85}, the unrestricted combination of \NF and embedded implication 
is particularly problematic, since it leads to the failure of basic
logic principles such as cut-elimination. We discuss this issue in
details in Section~\ref{sec:lamrelated}. 

At the user level, the presence of \nf in a \lf\ would make adequacy theorems
more difficult to establish, again because both provability and
unprovability now need to be considered.

In summary the adoption of \nf in a \lf\ seems to be a very risky, if
not hopeless road, considering its fragility already in the very
simple setting of Horn clauses.



