\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 elaborate a little, 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 manifesto ``Why Horn logic matters in 
	computer science" \cite{Ma8?}

	\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 as 
	built-ins, arithmetics I/O  (see the results in the Godel language)

	\item  The ``Making Prolog more expressive" bunch: to be pedantic, 
	this ought to be divided in two main  intertwined subtribues: the ``logicians",
	which claim that programming in Horn logic is like living with a 
	hand tightned behind, and the ``compilers" (see Sato and co. 
	\cite{Sa88}: 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 thru derivation and/or transformations from the 
	king of specifications language: \fo logic. For the logicians it is 
	a must to conquer any piece of land outside Horn logic, say by 
	adding connectives \cite{Poo85}, precompilation \cite{Llo85}, change 
	of interpreters (say connection graphs as in Gallier) or switching
	from classical logic to fragments in the intuitionistic galaxy 
	\cite{Gab85,Mac8?}\footnote{it would be instructive to follow this 
	path more closely, but we live this tasks to future historians, if 
	any.}.

	\item  Eventually 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 of features as modules, data abstraction and 
	scoping typical of other mature languages. An additional confirm of 
	the`rightness' of this view is the way in which linear logic 
	connectives as in Forum, \cite{Mil96}) have found a natural foundation
	 within UP.
\end{itemize}

It is nevertheless important to stress that other languages which 
share, at a certain extent, some of the features of UP---and I am 
referring mainly to Nprolog, IDC and PID---have gone into big 
troubles and have struggled to affirm themselves for reasons 
discussed elsewhere (\ref{uq}).