%Least Generalizations and Greatest Specializations of Sets of Clauses
%Shan-Hwei Nienhuys-Cheng and Ronald de Wolf
%For Journal of AI Research (JAIR)


\documentstyle[jair,twoside,11pt,theapa]{article}
\input epsf %% at top of file

\jairheading{4}{1996}{341-363}{11/95}{5/96}
\ShortHeadings{Least Generalizations and Greatest Specializations}
{Nienhuys-Cheng \& de Wolf}
\firstpageno{341}


\newtheorem{define}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}

\newenvironment{definition}
{\begin{define}\rm}
{{\hfill $\Box$}
 \end{define}}

\newenvironment{proof}
{\noindent {\bf Proof }}
{{\hfill $\Box$}\\
 \smallskip}

\newcommand{\lproof}{$\Leftarrow$:}
\newcommand{\rproof}{$\Rightarrow$:}

% like enumerate, but with less vertical space between items
\newenvironment{shortenum}
{\begin{enumerate}
 \setlength{\topsep}{0in}
 \setlength{\topskip}{0in}
 \setlength{\parskip}{0in}
 \setlength{\parsep}{0in}
 \setlength{\partopsep}{0in}
 \setlength{\itemsep}{0in}
 \vspace{-1ex}}
{\vspace{-1ex}
 \end{enumerate}}

% step in a binary resolution tree (conclusion)
\newcommand{\bintree}[1]{
\put(-50,60){\vector(1,-1){50}}
\put(50,60){\vector(-1,-1){50}}
\put(0,0){\makebox(0,0){#1}}
}




\begin{document}

\title{Least Generalizations and Greatest Specializations\\ of Sets of Clauses}

\author{\name Shan-Hwei Nienhuys-Cheng \email cheng@cs.few.eur.nl \\
       \name Ronald de Wolf \email bidewolf@cs.few.eur.nl \\
       \addr Erasmus University of Rotterdam\\
	     Department of Computer Science, H4-19\\
	     P.O.~Box 1738, 3000 DR Rotterdam, the Netherlands}

\maketitle



\begin{abstract}
The main operations in Inductive Logic Programming (ILP) are generalization 
and specialization, which only make sense in a generality order. 
In ILP, the three most important generality orders are subsumption, 
implication and implication relative to background knowledge. 
The two languages used most often are languages of clauses and languages of 
only Horn clauses. This gives a total of six different ordered languages.
In this paper, we give a systematic treatment of the existence or 
non-existence of least generalizations and greatest specializations
of finite sets of clauses in each of these six ordered sets.
We survey results already obtained by others and also contribute some 
answers of our own.

Our main new results are, firstly, the existence of a computable least 
generalization under implication of every finite set of clauses containing 
at least one non-tautologous function-free clause (among other, not 
necessarily function-free clauses).
Secondly, we show that such a least generalization need not exist under
relative implication, not even if both the set that is to be generalized
and the background knowledge are function-free.
Thirdly, we give a complete discussion of existence and non-existence of 
greatest specializations in each of the six ordered languages.
\end{abstract}






\section{Introduction}

Inductive Logic Programming (ILP) is a subfield of Logic Programming
and Machine Learning that tries to induce clausal theories from given
sets of positive and negative examples. An inductively inferred theory 
should imply all of the positive and none of the negative examples.
For instance, suppose we are given $P(0)$, $P(s^{2}(0))$, $P(s^{4}(0))$,
$P(s^{6}(0))$ as positive examples and $P(s(0)), P(s^{3}(0)), P(s^{5}(0))$ 
as negative examples.\footnote{Here $s^{2}(0)$ abbreviates $s(s(0))$, 
$s^{3}(0)$ abbreviates $s(s(s(0)))$, etc.}
Then the set $\Sigma=\{P(0),(P(s^{2}(x))\leftarrow P(x))\}$ 
is a solution: it implies all positive and no negative examples.
Note that this set can be seen as a description of the even integers,
learned from these examples. 
Thus induction of clausal theories is a form of learning from examples.
For a more extensive introduction to ILP, we refer to
\cite{lavrac&dzeroski94,muggleton&deraedt}. 

Learning from examples means modifying a theory to bring it more in 
accordance with the examples.
The two main operations in ILP for modification of a theory are 
{\em generalization} and {\em specialization}. 
Generalization strengthens a theory that is too weak, 
while specialization weakens a theory that is too strong.
These operations only make sense within a {\em generality order}.
This is a relation stating when some clause is more general than some other
clause.

The three most important generality orders used in ILP are subsumption 
(also called $\theta$-subsumption), logical implication and implication
relative to background knowledge.\footnote{There is also relative subsumption 
\cite{plotkin2}, which will be briefly touched in Section~\ref{secsubs}.}
In the subsumption order, we say that clause $C$ is more general than $D$---%
or, equivalently, $D$ is more specific than $C$---in case $C$ subsumes $D$.
In the implication order $C$ is more general than $D$ if $C$ logically 
implies $D$. Finally, $C$ is more general than $D$ relative to background 
knowledge $\Sigma$ ($\Sigma$ is a set of clauses), 
if $\{C\}\cup\Sigma$ logically implies $D$.

Of these three orders, subsumption is the most tractable.
In particular, subsumption is decidable, whereas logical implication is not 
decidable, not even for Horn clauses, as established by \fullciteA{marc&pach}.
In turn, relative implication is harder than implication:
both are undecidable, but proof procedures for implication
need to take only derivations from $\{C\}$ into account, whereas a proof
procedure for {\em relative} implication should check all derivations
from $\{C\}\cup\Sigma$.

Within a generality order, there are two approaches to generalization
or specialization. 
The first approach generalizes or specializes {\em individual} clauses. 
We do not discuss this in any detail in this paper, and merely
mention it for completeness' sake. 
This approach can be traced back to Reynolds' \citeyear{reynolds} concept 
of a {\em cover}. 
It was implemented for example by \fullciteA{shapiro81} in the subsumption 
order in the form of {\em refinement operators}. 
However, a clause $C$ which implies another clause $D$ need not subsume $D$. 
For instance, take $C=P(f(x))\leftarrow P(x)$ and 
$D=P(f^{2}(x))\leftarrow P(x)$. Then $C$ does not subsume $D$, but 
$C\models D$. Thus subsumption is weaker than implication.
A further sign of this weakness is the fact that tautologies need
not be subsume-equivalent, even though they are logically equivalent.

The second approach generalizes or specializes {\em sets} of clauses.
This is the approach we will be concerned with in this paper.
Here the concept of a {\em least generalization}\footnote{Least 
generalizations are also often called least {\em general} generalizations, 
for instance by \fullciteA{plotkin2,muggleton-selfsat,id-almq93,id-almq-jair,niblett}, 
though not by \fullciteA{plotkin1}, but we feel this `general' is redundant.}
is important. The use of such {\em least} generalizations allows us to 
generalize cautiously, avoiding over-generalization.
Least generalizations of sets of clauses were first discussed 
by \fullciteA{plotkin1,plotkin:phd,plotkin2}. He proved that any finite 
set $S$ of clauses has a least generalization under subsumption (LGS). 
This is a clause which subsumes all clauses in $S$ and which is subsumed 
by all other clauses that also subsume all clauses in $S$.
Positive examples can be generalized by taking their LGS.\footnote{There is 
also a relation between least generalization under subsumption and 
{\em inverse resolution} \cite{muggleton-ilp}.}
Of course, we need not take the LGS of {\em all} positive examples,
which would yield a theory consisting of only one clause.
Instead, we might divide the positive examples into subsets, 
and take a separate LGS of each subset. That way we obtain a theory
containing more than one clause.

For this second approach, subsumption is again not fully satisfactory.
For example, if $S$ consists of the clauses $D_{1}=P(f^{2}(a))\leftarrow P(a)$
and $D_{2}=P(f(b))\leftarrow P(b)$, then the LGS of $S$ is $P(f(y))\leftarrow
P(x)$. The clause $P(f(x))\leftarrow P(x)$, which seems more appropriate
as a least generalization of $S$, cannot be found by Plotkin's approach,
because it does not subsume $D_{1}$.
As this example also shows, the subsumption order is particularly 
unsatisfactory when we consider {\em recursive} clauses: clauses which can
be resolved with themselves.

Because of the weakness of subsumption, it is desirable to make the step 
from the subsumption order to the more powerful implication order.
Accordingly, it is important to find out whether Plotkin's positive 
result on the existence of LGS's holds for implication as well.
So far, the question whether any finite set of clauses has a least
generalization under implication (LGI) has only been partly answered.
For instance, \fullciteA{id-almq93,id-almq-jair} studies least 
generalizations under {\em T-implication} as an approximation to LGI's.
\fullciteA{muggleton-selfsat} investigate {\em self-saturated} clauses. 
A clause is self-saturated if it is subsumed by any clause which implies it. 
A clause $D$ is a self-saturation of $C$ if $C$ and $D$ are logically 
equivalent and $D$ is self-saturated.
As \fullciteA{muggleton-selfsat} state, if two clauses $C_{1}$ and $C_{2}$ 
have self-saturations $D_{1}$ and $D_{2}$, then an LGS of $D_{1}$ and
$D_{2}$ is also an LGI of $C_{1}$ and $C_{2}$. 
This positively answers our question concerning the existence of LGI's
in the case of clauses which have a self-saturation.
However, Muggleton and Page also show that there exist clauses which have 
no self-saturation. Hence the concept of self-saturation cannot solve 
our question in general.

Use of the third generality order, relative implication, is even more
desirable than the use of ``plain'' implication.
Relative implication allows us to take background knowledge into account,
which can be used to formalize many useful properties and relations of
the domain of application.
For this reason, least generalizations under implication relative to
background knowledge also deserve attention.

Apart from the least generalization, there is also its dual:
the {\em greatest specialization}. Greatest specializations have been
accorded much less attention in ILP than least generalizations, but the 
concept of a greatest specialization may nevertheless be useful
(see the beginning of Section~\ref{secgsi}).

In this paper, we give a systematic treatment of the existence and
non-existence of least generalizations and greatest specializations,
applied to each of these three generality orders.
Apart from distinguishing between these three orders, we also distinguish
between languages of general clauses and more restricted languages of Horn 
clauses.
Though most researchers in ILP restrict attention to Horn clauses,
general clauses are also sometimes used
\cite{plotkin1,plotkin2,shapiro81,deraedt&bruynooghe,id-almq93,id-almq-jair}.
Moreover, many researchers who do not use general clauses actually allow 
negative literals to appear in the body of a clause.
That is, they use clauses of the form $A\leftarrow L_{1},\ldots,L_{n}$,
where $A$ is an atom and each $L_{i}$ is a literal. These are
called {\em program} clauses \cite{lloyd87}.
Program clauses are in fact logically equivalent to general clauses.
For instance, the program clause $P(x)\leftarrow Q(x),\neg R(x)$ is 
equivalent to the non-Horn clause $P(x)\vee\neg Q(x)\vee R(x)$.
For these two reasons we consider not only languages of Horn clauses, 
but also pay attention to languages of general clauses.

The combination of three generality orders and two different possible
languages of clauses gives a total of six different ordered languages.
For each of these, we can ask whether least generalizations (LG's) 
and greatest specializations (GS's) always exist.
We survey results already obtained by others and also contribute some 
answers of our own. For the sake of clarity, we will summarize the 
results of our survey right at the outset.
In the following table `$+$' signifies a positive answer, 
and `$-$' means a negative answer.

\begin{table}[hbt]
\centering
\begin{tabular}{|l||c|c|c|c|}
\hline
 & \multicolumn{2}{|c|}{Horn clauses} & \multicolumn{2}{|c|}{General clauses}\\ \cline{2-5}
Quasi-order                               & LG  & GS  & LG  & GS\\ \hline
Subsumption ($\succeq$)                   & $+$ & $+$ & $+$ & $+$\\ \hline
Implication ($\models$)                   & $-$ & $-$ & $+$ for function-free & $+$\\ \hline
Relative implication ($\models_{\Sigma}$) & $-$ & $-$ & $-$ & $+$\\ \hline
\end{tabular}
\caption{Existence of LG's and GS's}
\label{lggstable}
\end{table}

Our own contributions to this table are threefold. First and foremost, 
we prove that if $S$ is a finite set of clauses containing at least one 
non-tautologous function-free clause\footnote{A clause which 
only contains constants and variables as terms.} (apart from this 
non-tautologous function-free clause, $S$ may contain an arbitrary finite
number of other clauses, including clauses which contain functions), then 
there exists a computable LGI of $S$.
This result is on the one hand based on the Subsumption Theorem for
resolution \cite{lee67,kowalski,cheng&wolf:f&f}, which allows us to 
restrict attention to finite sets of ground instances of clauses, and on the 
other hand on a modification of some proofs concerning T-implication which 
can be found in \cite{id-almq93,id-almq-jair}.
An immediate corollary of this result is the existence and computability
of an LGI of any finite set of function-free clauses.
As far as we know, both our general LGI-result and this particular corollary 
are new results.

\fullciteA[p.~135]{niblett} claims that ``it is simple to show 
that there are lggs if the language is restricted to a fixed set of 
constant symbols since all Herbrand interpretations are finite.''
Yet even for this special case of our general result, it appears 
that no proof has been published. Initially, we found a direct proof 
of this case, but this was not really any simpler than the proof of the
more general result that we give in this paper.
Niblett's idea that the proof is simple may be due to some confusion about
the relation between Herbrand models and logical implication (which is 
defined in terms of {\em all} models, not just Herbrand models).
We will describe this at the end of Subsection~\ref{existencelgi}.
Or perhaps one might think that the decidability of implication
for function-free clauses immediately implies the existence of an LGI.
But in fact, decidability is not a sufficient condition for the existence 
of a least generalization.
For example, it is decidable whether one function-free clause $C$ implies
another function-free clause $D$ relative to function-free background 
knowledge. Yet least generalizations relative to function-free background 
knowledge do not always exist, as we will show in Section~\ref{seclgr}.

Our LGI-result does not solve the general question of the existence of LGI's,
but it does provide a positive answer for a large class of cases:
the presence of one non-tautologous function-free clause in a finite $S$ 
already guarantees the existence and computability of an LGI of $S$, 
no matter what other clauses $S$ contains.\footnote{Note that even for 
function-free clauses, the subsumption order is still not enough.
Consider $D_{1}=P(x,y,z)\leftarrow P(y,z,x)$ and $D_{2}=P(x,y,z)\leftarrow
P(z,x,y)$ (this example is adapted from Idestam-Almquist). 
$D_{1}$ is a resolvent of $D_{2}$ and $D_{2}$ and $D_{2}$ is a resolvent
of $D_{1}$ and $D_{1}$. Hence $D_{1}$ and $D_{2}$ are logically equivalent. 
This means that $D_{1}$ is an LGI of the set $\{D_{1},D_{2}\}$.
However, the LGS of these two clauses is $P(x,y,z)\leftarrow P(u,v,w)$,
which is clearly an over-generalization.}
Because of the prominence of function-free clauses in ILP, this case may be 
of great practical signifcance.
Often, particularly in implementations of ILP-systems, the language is 
required to be function-free, or function symbols are removed from clauses
and put in the background knowledge by techniques such as 
{\em flattening} \cite{rouveirol}.
Well-known ILP-systems such as {\sc Foil} \cite{foil}, 
{\sc Linus} \cite{lavrac&dzeroski94} and {\sc Mobal} \cite{morikea:mobal}
all use only function-free clauses.
More than one half of the ILP-systems surveyed by \fullciteA{aha} is
restricted to function-free clauses. Function-free clauses are also 
sufficient for most applications concerning databases.

Our second contribution shows that a set $S$ need not have a least 
generalization relative to some background knowledge $\Sigma$, 
not even when $S$ and $\Sigma$ are both function-free.

Thirdly, we contribute a complete discussion of existence and non-existence 
of greatest specializations in each of the six ordered languages.
In particular, we show that any finite set of clauses has a greatest
specialization under implication. Combining this with the corollary of our 
result on LGI's, it follows that a function-free clausal language is a
{\em lattice}.






\section{Preliminaries} 

In this section we will define some of the concepts we need. 
For the definitions of `model', `tautology', `substitution', etc., we refer 
to standard works such as \cite{chang&lee73,lloyd87}.
A {\em positive literal} is an atom, a {\em negative literal} is the negation
of an atom. A {\em clause} is a finite set of literals, which is treated as
the universally quantified disjunction of those literals.
A {\em definite program clause} is a clause with one positive and zero or
more negative literals and a {\em definite goal} is a clause without 
positive literals.
A {\em Horn clause} is either a definite program clause or a definite goal.
If $C$ is a clause, we use $C^{+}$ to denote the positive literals in $C$,
and $C^{-}$ to denote the negative literals in $C$.
The empty clause, which represents a contradiction, is denoted by $\Box$.

\begin{definition}
Let $\cal A$ be an alphabet of the first-order logic.
Then the {\em clausal language $\cal C$ by $\cal A$} is the set of all
clauses which can be constructed from the symbols in $\cal A$.
The {\em Horn language $\cal H$ by $\cal A$} is the set of all
Horn clauses which can be constructed from the symbols in $\cal A$.
\end{definition}

\noindent In this paper, we just presuppose some arbitrary alphabet $\cal A$, 
and consider the clausal language $\cal C$ and Horn language $\cal H$
based on this $\cal A$.
We will now define three increasingly strong generality orders on clauses: 
subsumption, implication and relative implication.

\begin{definition}
Let $C$ and $D$ be clauses and $\Sigma$ be a set of clauses.
We say that $C$ {\em subsumes} $D$, denoted as $C\succeq D$, if there exists 
a substitution $\theta$ such that $C\theta\subseteq D$.\footnote{Right
from the very first applications of subsumption in ILP, there has been some 
controversy about the symbol used for subsumption: \fullciteA{plotkin1} 
used `$\leq$', while \fullciteA{reynolds} used `$\geq$'.
We use `$\succeq$' here, similar to Reynolds' `$\geq$', because we feel it 
serves the intuition to view $C$ as somehow ``bigger'' or ``stronger'' than 
$D$, if $C\succeq D$ holds.}
$C$ and $D$ are {\em subsume-equivalent} if $C\succeq D$ and $D\succeq C$.

$\Sigma$ {\em (logically) implies $C$}, denoted as $\Sigma\models C$,
if every model of $\Sigma$ is also a model of $C$.
$C$ {\em (logically) implies $D$}, denoted as $C\models D$, if 
$\{C\}\models D$. $C$ and $D$ are {\em (logically) equivalent} if 
$C\models D$ and $D\models C$.

$C$ {\em implies $D$ relative to $\Sigma$}, denoted as 
$C\models_{\Sigma} D$, if $\Sigma\cup\{C\}\models D$. $C$ and $D$ are 
{\em equivalent relative to $\Sigma$} if $C\models_{\Sigma}D$ and 
$D\models_{\Sigma}C$.
\end{definition}

\noindent If $C$ does not subsume $D$, we write $C\not\succeq D$.
Similarly, we use the notation $C\not\models D$ and $C\not\models_{\Sigma}D$.

If $C\succeq D$, then $C\models D$. 
The converse does not hold, as the examples in the introduction showed.
Similarly, if $C\models D$, then $C\models_{\Sigma}D$, and again the
converse need not hold. Consider $C=P(a)\vee\neg P(b)$, $D=P(a)$,
and $\Sigma=\{P(b)\}$: then $C\models_{\Sigma}D$, but $C\not\models D$.

We now proceed to define a proof procedure for logical implication between
clauses, using resolution and subsumption.

\begin{definition}
If two clauses have no variables in common, then they are said to
be {\em standardized apart}.

Let $C_{1}=L_{1}\vee\ldots\vee L_{i}\vee\ldots\vee L_{m}$ and 
$C_{2}=M_{1}\vee\ldots\vee M_{j}\vee\ldots\vee M_{n}$ be two clauses
which are standardized apart.
If the substitution $\theta$ is a most general unifier (mgu) of the set 
$\{L_{i},\neg M_{j}\}$, then the clause $((C_{1}-L_{i})\cup (C_{2}-M_{j}))
\theta$ is called a {\em binary resolvent} of $C_{1}$ and $C_{2}$. 
The literals $L_{i}$ and $M_{j}$ are said to be the literals {\em resolved upon}. 
\end{definition}

\noindent If $C_{1}$ and $C_{2}$ are not standardized apart, we can take
a variant $C'_{2}$ of $C_{2}$, such that $C_{1}$ and $C'_{2}$ are 
standardized apart. For simplicity, a binary resolvent of $C_{1}$ and 
$C'_{2}$ is also called a binary resolvent of $C_{1}$ and $C_{2}$ itself.

\begin{definition}
Let $C$ be a clause and $\theta$ an mgu of $\{L_{1},\ldots,L_{n}\}
\subseteq C$ ($n\geq 1$).
Then the clause $C\theta$ is called a {\em factor} of $C$.
\end{definition}

\noindent Note that any non-empty clause $C$ is a factor of itself, using the 
empty substitution $\varepsilon$ as an mgu of a single literal in $C$.

\begin{definition}
A {\em resolvent} $C$ of clauses $C_{1}$ and $C_{2}$ is a binary resolvent 
of a factor of $C_{1}$ and a factor of $C_{2}$, where the literals resolved 
upon are the literals unified in the respective factors.
$C_{1}$ and $C_{2}$ are the {\em parent clauses} of $C$.
\end{definition}

\begin{definition}
Let $\Sigma$ be a set of clauses and $C$ a clause.
A {\em derivation} of $C$ from $\Sigma$ is a finite sequence of clauses 
$R_{1},\ldots,R_{k}=C$, such that each $R_{i}$ is either in $\Sigma$, or a 
resolvent of two clauses in $\{R_{1},\ldots,R_{i-1}\}$.
If such a derivation exists, we write $\Sigma\vdash_{r}C$.
\end{definition}

\begin{definition}
Let $\Sigma$ be a set of clauses and $C$ a clause.
We say there exists a {\em deduction} of $C$ from $\Sigma$, written as
$\Sigma\vdash_{d}C$, if $C$ is a tautology, or if there exists a clause $D$
such that $\Sigma\vdash_{r}D$ and $D\succeq C$.
\end{definition}

\noindent The next result, proved by \fullciteA{cheng&wolf:f&f},
generalizes Herbrand's Theorem:

\begin{theorem}\label{groundlogq}
Let $\Sigma$ be a set of clauses and $C$ be a ground clause.
If $\Sigma\models C$, then there exists a finite set $\Sigma_{g}$ of ground 
instances of clauses in $\Sigma$, such that $\Sigma_{g}\models C$.
\end{theorem}

\noindent The following Subsumption Theorem gives a precise characterization 
of implication between clauses in terms of resolution and subsumption.
It was proved by \fullciteA{lee67,kowalski} and reproved by 
\fullciteA{cheng&wolf:f&f}.

\begin{theorem}[Subsumption theorem]\label{lee}
Let $\Sigma$ be a set of clauses and $C$ be a clause. 
Then $\Sigma\models C$ iff $\Sigma\vdash_{d}C$.
\end{theorem}

\noindent The next lemma was first proved by \fullciteA{gottlob}.
Actually, it is an immediate corollary of the subsumption theorem:

\begin{lemma}[Gottlob]\label{gottlob}
Let $C$ and $D$ be non-tautologous clauses.
If $C\models D$, then $C^{+}\succeq D^{+}$ and $C^{-}\succeq D^{-}$. 
\end{lemma}

\begin{proof}
Since $C^{+}\succeq C$, if $C\models D$, then we have $C^{+}\models D$.
Since $C^{+}$ cannot be resolved with itself, it follows from the 
subsumption theorem that $C^{+}\succeq D$.
But then $C^{+}$ must subsume the positive literals in $D$, 
hence $C^{+}\succeq D^{+}$. Similarly $C^{-}\succeq D^{-}$. 
\end{proof}

\noindent An important consequence of this lemma concerns the {\em depth}
of clauses, defined as follows:

\begin{definition}
Let $t$ be a term. If $t$ is a variable or constant, 
then the {\em depth} of $t$ is 1. 
If $t=f(t_{1},\ldots,t_{n})$, $n\geq 1$, then the depth of $t$ is 
1 plus the depth of the $t_{i}$ with largest depth.
The {\em depth} of a clause $C$ is the depth of the term with largest
depth in $C$.
\end{definition}

\noindent For example, the term $t=f(a,x)$ has depth 2.
$C=P(f(x))\leftarrow P(g(f(x),a))$ has depth 3, since $g(f(x),a)$ has depth 3.
It follows from Gottlob's lemma that if $C\models D$,
then the depth of $C$ is smaller than or equal to the depth of $D$,
for otherwise $C^{+}$ cannot subsume $D^{+}$ or $C^{-}$ cannot subsume $D^{-}$. 
For instance, take $D=P(x,f(x,g(y)))\leftarrow P(g(a),b)$, which has depth 3.
Then a clause $C$ containing a term $f(x,g^{2}(y))$ (depth 4) cannot imply $D$.

\begin{definition}
Let $S$ and $S'$ be finite sets of clauses,
$x_{1},\ldots,x_{n}$ all distinct variables appearing in $S$, 
and $a_{1},\ldots,a_{n}$ distinct constants not appearing in $S$ or $S'$.
Then $\sigma=\{x_{1}/a_{1},\ldots,x_{n}/a_{n}\}$ is called a
{\em Skolem substitution} for $S$ w.r.t.\ $S'$.
If $S'$ is empty, we just say that $\sigma$ is a Skolem substitution for $S$.
\end{definition}

\begin{lemma}\label{skolemimpl}
Let $\Sigma$ be a set of clauses, $C$ be a clause,
and $\sigma$ be a Skolem substitution for $C$ w.r.t.\ $\Sigma$. 
Then $\Sigma\models C$ iff $\Sigma\models C\sigma$.
\end{lemma}

\begin{proof}

\rproof\
Obvious.

\lproof\
Suppose $C$ is not a tautology and let 
$\sigma=\{x_{1}/a_{1},\ldots,x_{n}/a_{n}\}$.
If $\Sigma\models C\sigma$, it follows from the subsumption theorem that
there is a $D$ such that $\Sigma\vdash_{r}D$ and $D\succeq C\sigma$. 
Thus there is a $\theta$, such that $D\theta\subseteq C\sigma$.
Note that since $\Sigma\vdash_{r}D$ and none of the constants $a_{1},\ldots,
a_{n}$ appears in $\Sigma$, none of these constants appears in $D$.
Now let $\theta'$ be obtained by replacing in $\theta$ all occurrences of 
$a_{i}$ by $x_{i}$, for every $1\leq i\leq n$.
Then $D\theta'\subseteq C$, hence $D\succeq C$.
Therefore $\Sigma\vdash_{d}C$ and hence $\Sigma\models C$. 
\end{proof}






\section{Least Generalizations and Greatest Specializations}

In this section, we will define the concepts we need concerning 
least generalizations and greatest specializations.

\begin{definition}
Let $\Gamma$ be a set and $R$ be a binary relation on $\Gamma$.
\begin{shortenum}
\item $R$ is {\em reflexive on $\Gamma$}, if $xRx$ for every $x\in\Gamma$.
\item $R$ is {\em transitive on $\Gamma$}, if for every $x,y,z\in\Gamma$,
$xRy$ and $yRz$ implies $xRz$.
\item $R$ is {\em symmetric on $\Gamma$}, if for every $x,y\in\Gamma$,
$xRy$ implies $yRx$.
\item $R$ is {\em anti-symmetric on $\Gamma$}, if for every $x,y,z\in\Gamma$,
$xRy$ and $yRx$ implies $x=y$.
\end{shortenum}
If $R$ is both reflexive and transitive on $\Gamma$, 
we say $R$ is a {\em quasi-order} on $\Gamma$.
If $R$ is both reflexive, transitive and anti-symmetric on $\Gamma$, 
we say $R$ is a {\em partial order} on $\Gamma$.
If $R$ is reflexive, transitive and symmetric on $\Gamma$, 
$R$ is an {\em equivalence relation} on $\Gamma$.
\end{definition}

\noindent 
A quasi-order $R$ on $\Gamma$ induces an equivalence-relation $\sim$ on 
$\Gamma$, as follows: we say $x,y\in\Gamma$ are {\em equivalent} induced by
$R$ (denoted $x\sim y$) if both $xRy$ and $yRx$.
Using this equivalence relation, a quasi-order $R$ on $\Gamma$ induces a
partial order $R'$ on the set of equivalence classes in $\Gamma$,
defined as follows: if $[x]$ denotes the equivalence class of $x$ 
(i.e., $[x]=\{y\mbox{ $|$ } x\sim y\}$), then $[x]R'[y]$ iff $xRy$.

We first give a general definition of least generalizations and greatest
specializations for sets of clauses ordered by some quasi-order, which we 
then instantiate in different ways.

\begin{definition}\label{deflggs}
Let $\Gamma$ be a set of clauses, $\geq$ be a quasi-order on $\Gamma$,
$S\subseteq\Gamma$ be a finite set of clauses and $C\in\Gamma$.
If $C\geq D$ for every $D\in S$, then we say $C$ is a 
{\em generalization} of $S$ under $\geq$. 
Such a $C$ is called a {\em least generalization (LG)} of $S$ under 
$\geq$ in $\Gamma$, if we have $C'\geq C$ for every 
generalization $C'\in\Gamma$ of $S$ under $\geq$.

Dually, $C$ is a {\em specialization} of $S$ under $\geq$,
if $D\geq C$ for every $D\in S$.
Such a $C$ is called a {\em greatest specialization (GS)} of $S$ under
$\geq$ in $\Gamma$, if we have $C\geq C'$ for every 
specialization $C'\in\Gamma$ of $S$ under $\geq$.
\end{definition}

\noindent It is easy to see that if some set $S$ has an LG or
GS under $\geq$ in $\Gamma$, then this LG or GS will be unique
up to the equivalence induced by $\geq$ in $\Gamma$.
That is, if $C$ and $D$ are both LG's or GS's of some set $S$, 
then we have $C\sim D$. 

The concepts defined above are instances of the mathematical concepts of
(least) upper bounds and (greatest) lower bounds. Thus we can speak of
lattice-properties of a quasi- or partially ordered set of clauses: 

\begin{definition}
Let $\Gamma$ be a set of clauses and $\geq$ be a quasi-order on $\Gamma$.
If for every finite subset $S$ of $\Gamma$, there exist both a least 
generalization and a greatest specialization of $S$ under $\geq$ in $\Gamma$, 
then the set $\Gamma$ ordered by $\geq$ is called a {\em lattice}.
\end{definition}

\noindent It should be noted that usually in mathematics, a lattice is
defined for a partial order instead of a quasi-order. However, since 
in ILP we usually have to deal with individual clauses rather than with 
equivalence classes of clauses, it is convenient for us to define `lattice' 
for a quasi-order here.
Anyhow, if a quasi-order $\geq$ is a lattice on $\Gamma$, then the
partial order induced by $\geq$ is a lattice on the set of equivalence
classes in $\Gamma$.

In ILP, there are two main instantiations for the set of clauses $\Gamma$: 
either we take a clausal language $\cal C$, or we take a Horn language 
$\cal H$. Similarly, there are three interesting choices for the quasi-order 
$\geq$: we can use either $\succeq$ (subsumption), $\models$ 
(implication), or $\models_{\Sigma}$ (relative implication) for some 
background knowledge $\Sigma$.
In the $\succeq$-order, we will sometimes abbreviate the terms `least 
generalization of $S$ under subsumption' and `greatest specialization of $S$
under subsumption' to `LGS of $S$' and `GSS of $S$', respectively.
Similarly, in the $\models$-order we will sometimes speak of an LGI 
(least generalization under implication) and a GSI.
In the $\models_{\Sigma}$-order, we will use LGR (least generalization under
{\em relative} implication) and GSR.

These two different languages and three different quasi-orders give a total
of six combinations. For each combination, we can ask whether an LG or GS 
of every finite set $S$ exists.
In the next section, we will review the answers for subsumption
given by others or by ourselves. 
Then we devote two sections to least generalizations and greatest 
specializations under implication, respectively.
Finally, we discuss least generalizations and greatest specializations
under relative implication.
The results of this survey have already been summarized in 
Table~\ref{lggstable} in the introduction.





\section{Subsumption}\label{secsubs}

First we devote some attention to subsumption.
Least generalizations under subsumption have been discussed extensively 
by \fullciteA{plotkin1}.
The main result in Plotkin's framework is the following:

\begin{theorem}[Existence of LGS in ${\cal C}$]
Let $\cal C$ be a clausal language.
Then for every finite $S\subseteq\cal C$, there exists an LGS of $S$
in $\cal C$.
\end{theorem}

\noindent If $S$ only contains Horn clauses, then it can be shown that the 
LGS of $S$ is itself also a Horn clause. Thus the question for the existence
of an LGS of every finite set $S$ of clauses is answered positively
for both clausal languages and for Horn languages.

Plotkin established the existence of an LGS, but he seems to have 
ignored the GSS in \citeyear{plotkin1,plotkin2}, possibly because it is a 
very straightforward result.
It is in fact fairly easy to show that the GSS of some finite set $S$ of 
clauses is simply the union of all clauses in $S$ after they are
standardized apart.\footnote{Note that this has nothing to do with 
{\em unification}. For instance, if $S=\{P(a,x), P(y,b)\}$, then the GSS
of $S$ in $\cal C$ would be $P(a,x)\vee P(y,b)$.
However, if we would instantiate $\Gamma$ in Definition~\ref{deflggs}
to the set of atoms, then the greatest specialization of two atoms
{\em in the set of atoms} should itself also be an atom. The GSS of two
atoms is then their most general unification \cite{reynolds}.
For instance, the GSS of $S$ would in this case be $P(a,b)$.}
We include the proof here.

\begin{theorem}[Existence of GSS in ${\cal C}$]
Let $\cal C$ be a clausal language.
Then for every finite $S\subseteq\cal C$, there exists a GSS of $S$
in $\cal C$.
\end{theorem}

\begin{proof}
Suppose $S=\{D_{1},\ldots,D_{n}\}\subseteq\cal C$. Without loss of 
generality, we assume the clauses in $S$ are standardized apart.
Let $D=D_{1}\cup\ldots\cup D_{n}$, then $D_{i}\succeq D$, for every
$1\leq i\leq n$.
Now let $C\in\cal C$ be such that $D_{i}\succeq C$, for every $1\leq i\leq n$.
Then for every $1\leq i\leq n$, there is a $\theta_{i}$ such that $D_{i}
\theta_{i}\subseteq C$ and $\theta_{i}$ only acts on variables in $D_{i}$.
If we let $\theta=\theta_{1}\cup\ldots\cup\theta_{n}$,
then $D\theta=D_{1}\theta_{1}\cup\ldots\cup D_{n}\theta_{n}\subseteq C$.
Hence $D\succeq C$, so $D$ is a GSS of $S$ in $\cal C$.
\end{proof}

\noindent This establishes that a clausal language $\cal C$ ordered by 
$\succeq$ is a lattice. 

Proving the existence of a GSS of every finite set of Horn clauses in 
$\cal H$ requires a little more work, but here also the result is positive.
For example, $D=P(a)\leftarrow P(f(a)),Q(y)$ is a GSS of
$D_{1}=P(x)\leftarrow P(f(x))$ and $D_{2}=P(a)\leftarrow Q(y)$.
Note that $D$ can be obtained by applying $\sigma=\{x/a\}$ (the mgu of
the heads of $D_{1}$ and $D_{2}$) to $D_{1}\cup D_{2}$, the GSS of 
$D_{1}$ and $D_{2}$ in $\cal C$.
This idea will be used in the following proof.
Here we assume ${\cal H}$ contains an artificial bottom element (True) 
$\bot$, such that $C\succeq\bot$ for every $C\in\cal H$,
and $\bot\not\succeq C$ for every $C\neq\bot$. 
Note that $\bot$ is not subsume-equivalent with other tautologies.

\begin{theorem}[Existence of GSS in ${\cal H}$]
Let $\cal H$ be a Horn language, with $\bot\in\cal H$.
Then for every finite $S\subseteq\cal H$, there exists a GSS of $S$
in $\cal H$.
\end{theorem}

\begin{proof}
Suppose $S=\{D_{1},\ldots,D_{n}\}\subseteq\cal H$.
Without loss of generality we assume the clauses in $S$ are standardized
apart, $D_{1},\ldots,D_{k}$ are the definite program clauses in $S$, and
$D_{k+1},\ldots,D_{n}$ are the definite goals in $S$.
If $k=0$ (i.e., if $S$ only contains goals), then it is easy to show that 
$D_{1}\cup\ldots\cup D_{n}$ is a GSS of $S$ in $\cal H$.
If $k\geq 1$ and the set $\{D_{1}^{+},\ldots,D_{k}^{+}\}$ is not unifiable, 
then $\bot$ is a GSS of $S$ in $\cal H$.
Otherwise, let $\sigma$ be an mgu of $\{D_{1}^{+},\ldots,D_{k}^{+}\}$, 
and let $D=D_{1}\sigma\cup\ldots\cup D_{n}\sigma$ (note that actually
$D_{i}\sigma=D_{i}$ for $k+1\leq i\leq n$, since the clauses in $S$ are
standardized apart). 
Since $D$ has exactly one literal in its head, it is a definite program 
clause. Furthermore, we have $D_{i}\succeq D$ for every $1\leq i\leq n$,
since $D_{i}\sigma\subseteq D$. 

To show that $D$ is a GSS of $S$ in $\cal H$, suppose $C\in\cal H$ is some 
clause such that $D_{i}\succeq C$ for every $1\leq i\leq n$. 
For every $1\leq i\leq n$, let $\theta_{i}$ be such that 
$D_{i}\theta_{i}\subseteq C$ and $\theta_{i}$ only acts on variables in 
$D_{i}$. Let $\theta=\theta_{1}\cup\ldots\cup\theta_{n}$.
For every $1\leq i\leq k$, $D_{i}^{+}\theta=D_{i}^{+}\theta_{i}=C^{+}$, so 
$\theta$ is a unifier of $\{D_{1}^{+},\ldots,D_{k}^{+}\}$. 
But $\sigma$ is an mgu of this set, so there is a $\gamma$ such that
$\theta=\sigma\gamma$.
Now $D\gamma=D_{1}\sigma\gamma\cup\ldots\cup D_{n}\sigma\gamma=
D_{1}\theta\cup\ldots\cup D_{n}\theta=
D_{1}\theta_{1}\cup\ldots\cup D_{n}\theta_{n}\subseteq C$. 
Hence $D\succeq C$, so $D$ is a GSS of $S$ in $\cal H$.
See figure~\ref{hgssfig} for illustration of the case where $n=2$.

\begin{figure}[hbt]
\centering
\setlength{\unitlength}{0.25mm}
\begin{picture}(130,89)
{\scriptsize

\put(0,0){
\begin{picture}(130,89)
\put(4,89){\makebox(0,0){$D_{1}$}}
\put(10,83){\vector(2,-1){50}}
\put(35,75){\makebox(0,0){$\sigma$}}
\put(10,83){\vector(2,-3){50}}
\put(36,28){\makebox(0,0){$\theta_{1}$}}
\put(126,89){\makebox(0,0){$D_{2}$}}
\put(120,83){\vector(-2,-1){50}}
\put(95,75){\makebox(0,0){$\sigma$}}
\put(120,83){\vector(-2,-3){50}}
\put(95,28){\makebox(0,0){$\theta_{2}$}}
\put(65,50){\makebox(0,0){$D$}}
\put(65,41){\vector(0,-1){33}}
\put(70,28){\makebox(0,0){$\gamma$}}
\put(65,0){\makebox(0,0){$C$}}
\end{picture}}
}
\end{picture}
\caption{$D$ is a GSS of $D_{1}$ and $D_{2}$}
\label{hgssfig}
\end{figure}
\end{proof}

\noindent 
Thus a Horn language $\cal H$ ordered by $\succeq$ is also a lattice.

We end this section by briefly discussing Plotkin's 
\citeyear{plotkin2} {\em relative subsumption}.
This is an extension of subsumption which takes background knowledge
into account. This background knowledge is rather restricted: 
it must be a finite set $\Sigma$ of {\em ground literals}. 
Because of its restrictiveness, we have not included relative subsumption 
in Table~\ref{lggstable}.
Nevertheless, we mention it here, because least generalization under
relative subsumption forms the basis of the well-known ILP system 
{\sc Golem}~\cite{muggleton-golem}.

\begin{definition}
Let $C,D$ be clauses, $\Sigma=\{L_{1},\ldots,L_{m}\}$ be 
a finite set of ground literals.
Then {\em $C$ subsumes $D$ relative to $\Sigma$}, denoted by 
$C\succeq_{\Sigma}D$, if $C\succeq(D\cup\{\neg L_{1},\ldots,\neg L_{m}\})$.
\end{definition}

\noindent It is easy to see that $\succeq_{\Sigma}$ is reflexive and
transitive, so it imposes a quasi-order on a set of clauses.

Suppose $S=\{D_{1},\ldots,D_{n}\}$ and $\Sigma=\{L_{1},\ldots,L_{m}\}$. 
It is easy to see that an LGS of 
$\{(D_{1}\cup\{\neg L_{1},\ldots,\neg L_{m}\}),\ldots,
(D_{n}\cup\{\neg L_{1},\ldots,\neg L_{m}\})\}$ is a least generalization
of $S$ under $\succeq_{\Sigma}$, so every finite set of clauses
has a least generalization under $\succeq_{\Sigma}$ in $\cal C$.
Moreover, if each $D_{i}$ is a Horn clause and each $L_{j}$ is a 
{\em positive} ground literal (i.e., a ground atom), then this least 
generalization will itself also be a Horn clause.
Accordingly, if $\Sigma$ is a finite set of positive ground literals, then
every finite set of Horn clauses has a least generalization under 
$\succeq_{\Sigma}$ in $\cal H$.







\section{Least Generalizations under Implication}

Now we turn from subsumption to the implication order.
In this section we will discuss LGI's, in the next section we handle GSS's.
For Horn clauses, the LGI-question has already been answered negatively
by \fullciteA{muggleton&deraedt}.

Let $D_{1}=P(f^{2}(x))\leftarrow P(x)$, $D_{2}=P(f^{3}(x))\leftarrow P(x)$,
$C_{1}=P(f(x))\leftarrow P(x)$ and $C_{2}=P(f^{2}(y))\leftarrow P(x)$.
Then we have both $C_{1}\models\{D_{1},D_{2}\}$ and $C_{2}\models\{D_{1},D_{2}\}$.
It is not very difficult to see that there are no more specific Horn clauses 
than $C_{1}$ and $C_{2}$ that imply both $D_{1}$ and $D_{2}$.
For $C_{1}$: no resolvent of $C_{1}$ with itself implies $D_{2}$ and no 
clause that is properly subsumed by $C_{1}$ still implies $D_{1}$ and $D_{2}$.
For $C_{2}$: every resolvent of $C_{2}$ with itself is a variant of $C_{2}$,
and no clause that is properly subsumed by $C_{2}$ still implies $D_{1}$ and
$D_{2}$. Thus $C_{1}$ and $C_{2}$ are both ``minimal'' generalizations under 
implication of $\{D_{1},D_{2}\}$.
Since $C_{1}$ and $C_{2}$ are not logically equivalent under implication, 
there is no LGI of $\{D_{1},D_{2}\}$ in $\cal H$.

However, the fact that there is no LGI of $\{D_{1},D_{2}\}$ in $\cal H$
does not mean that $D_{1}$ and $D_{2}$ have no LGI in $\cal C$, 
since a Horn language is a more restricted space than a clausal language. 
In fact, it is shown by \fullciteA{muggleton-selfsat} that
$C=P(f(x))\vee P(f^{2}(y))\leftarrow P(x)$ is an LGI of $D_{1}$ and $D_{2}$
in $\cal C$. For this reason, it may be worthwhile for the LGI
to consider a clausal language instead of only Horn clauses.

In the next subsection, we show that any finite set of clauses which contains 
at least one non-tautologous function-free clause, has an LGI in $\cal C$.
An immediate corollary of this result is the existence of an LGI of 
any finite set of function-free clauses.
In our usage of the word, a `function-free' clause may contain constants,
even though constants are sometimes seen as functions of arity 0.

\begin{definition}
A clause is {\em function-free} if it does not contain function symbols
of arity 1 or more.
\end{definition}

\noindent Note that a clause is function-free iff it has depth 1.
In case of sets of clauses which all contain function symbols, 
the LGI-question remains open.



\subsection{A Sufficient Condition for the Existence of an LGI}\label{existencelgi}

In this subsection, we will show that any finite set $S$ of clauses containing
at least one non-tautologous function-free clause, has an LGI in $\cal C$.

\begin{definition}
Let $C$ be a clause, $x_{1},\ldots,x_{n}$ all distinct variables in $C$,
and $K$ a set of terms.
Then the {\em instance set} of $C$ w.r.t.\ $K$ is ${\cal I}(C,K)=
\{C\theta\mbox{ $|$ }\theta=\{x_{1}/t_{1},\ldots,x_{n}/t_{n}\},$ 
where $t_{i}\in K$, for every $1\leq i\leq n\}$.
If $\Sigma=\{C_{1},\ldots,C_{k}\}$ is a set of clauses, 
then the {\em instance set} of $\Sigma$ w.r.t.\ $K$ is 
${\cal I}(\Sigma,K)={\cal I}(C_{1},K)\cup\ldots\cup{\cal I}(C_{k},K)$.
\end{definition}

\noindent For example, if $C=P(x)\vee Q(y)$ and $T=\{a,f(z)\}$, then
${\cal I}(C,T)=\{(P(a)\vee Q(a)), (P(a)\vee Q(f(z))), (P(f(z))\vee Q(a)),
(P(f(z))\vee Q(f(z)))\}$.

\begin{definition}
Let $S$ be a finite set of clauses,
and $\sigma$ be a Skolem substitution for $S$. 
Then the {\em term set} of $S$ by $\sigma$ is the set of all terms 
(including subterms) occurring in $S\sigma$.
\end{definition}

\noindent A term set of $S$ by some $\sigma$ is a finite set of ground terms. 
For instance, the term set of $D=P(f^{2}(x),y,z)\leftarrow P(y,z,f^{2}(x))$ 
by $\sigma=\{x/a,y/b,z/c\}$ is $T=\{a,f(a),f^{2}(a),b,c\}$.

Our definition of a term set corresponds to what 
\fullciteA{id-almq93,id-almq-jair} calls a `minimal term set'. 
In his definition, if $\sigma$ is a Skolem
substitution for a set of clauses $S=\{D_{1},\ldots,D_{n}\}$ w.r.t.\ some 
other set of clauses $S'$, then a {\em term set} of $S$ is a finite set of 
terms which contains the minimal term set of $S$ by $\sigma$ as a subset.

Using his notion of term set, he defines {\em T-implication} as follows: 
if $C$ and $D$ are clauses and $T$ is a term set of $\{D\}$ by 
some Skolem substitution $\sigma$ w.r.t.\ $\{C\}$, then $C$ {\em T-implies} 
$D$ w.r.t.\ $T$ if ${\cal I}(C,T)\models D\sigma$.
T-implication is decidable, weaker than logical implication and stronger
than subsumption. 
\fullciteA{id-almq93,id-almq-jair} gives the result that any finite set of 
clauses has a least generalization under T-implication w.r.t.\ any term set $T$.
However, as he also notes, T-implication is not transitive and hence not a 
quasi-order. Therefore it does not fit into our general framework here. 
For this reason, we will not discuss it fully here, and for the same reason 
we have not included a row for T-implication in Table~\ref{lggstable}.

Let us now begin with the proof of our result concerning the existence of LGI's.
Consider $C=P(x,y,z)\leftarrow P(z,x,y)$ and $D$, $\sigma$ and $T$ as above. 
Then $C\models D$ and also ${\cal I}(C,T)\models D\sigma$, since
$D\sigma$ is a resolvent of $P(f^{2}(a),b,c)\leftarrow P(c,f^{2}(a),b)$ and 
$P(c,f^{2}(a),b)\leftarrow P(b,c,f^{2}(a))$, which are in ${\cal I}(C,T)$.
As we will show in the next lemma, this holds in general: if $C\models D$ and 
$C$ is function-free, then we can restrict attention to the ground instances 
of $C$ instantiated to terms in the term set of $D$ by some $\sigma$.

The proof of Lemma~\ref{sufftermset} uses the following idea.
Consider a derivation of a clause $E$ from a set $\Sigma$ of ground clauses.
Suppose some of the clauses in $\Sigma$ contain terms not appearing in $E$.
Then any literals containing these terms in $\Sigma$ must be resolved away 
in the derivation.
This means that if we replace all the terms in the derivation that are not 
in $E$, by some other term $t$, then the result will 
be another derivation of $E$. For example, the left of 
figure~\ref{sigandsig'} shows a derivation of length 1 of $E$. 
The term $f^{2}(b)$ in the parent clauses does not appear in $E$.
If we replace this term by the constant $a$, 
the result is another derivation of $E$ (right of the figure).

\begin{figure}[hbt]
\centering
\setlength{\unitlength}{0.2mm}
\begin{picture}(430,75)
{\scriptsize

\put(0,0){
\begin{picture}(150,70)
\put(0,70){\makebox(0,0){$P(b)\leftarrow P(f^{2}(b))$}}
\put(150,70){\makebox(0,0){$P(f^{2}(b))\leftarrow Q(a,f(a))$}}
\put(70,0){\bintree{$E=P(b)\leftarrow Q(a,f(a))$}}
\end{picture}}

\put(310,0){
\begin{picture}(120,70)
\put(-10,70){\makebox(0,0){$P(b)\leftarrow P(a)$}}
\put(120,70){\makebox(0,0){$P(a)\leftarrow Q(b,f(a))$}}
\put(60,0){\bintree{$E=P(b)\leftarrow Q(a,f(a))$}}
\end{picture}}
}
\end{picture}
\caption{Transforming the left derivation yields the right derivation}
\label{sigandsig'}
\end{figure}

\begin{lemma}\label{sufftermset}
Let $C$ be a function-free clause, $D$ be a clause, $\sigma$ be a Skolem
substitution for $D$ w.r.t.\ $\{C\}$ and $T$ be the term set of $D$ by 
$\sigma$. Then $C\models D$ iff ${\cal I}(C,T)\models D\sigma$.
\end{lemma}

\begin{proof}

\lproof\
Since $C\models{\cal I}(C,T)$ and ${\cal I}(C,T)\models D\sigma$, 
we have $C\models D\sigma$. Now $C\models D$ by Lemma~\ref{skolemimpl}.

\rproof\
If $D$ is a tautology, then $D\sigma$ is a tautology, so this case is obvious.
Suppose $D$ is not a tautology, then $D\sigma$ is not a tautology.
Since $C\models D\sigma$, it follows from Theorem~\ref{groundlogq} that 
there exists a finite set $\Sigma$ of ground instances of $C$, such that 
$\Sigma\models D\sigma$.
By the Subsumption Theorem, there exists a derivation from $\Sigma$ of a 
clause $E$, such that $E\succeq D\sigma$. Since $\Sigma$ is ground, 
$E$ must also be ground, so we have $E\subseteq D\sigma$. 
This implies that $E$ only contains terms from $T$.

Let $t$ be an arbitrary term in $T$ and let $\Sigma'$ be obtained from 
$\Sigma$ by replacing every term in clauses in $\Sigma$ which is not in $T$, 
by $t$. Note that since each clause in $\Sigma$ is a ground instance of the
function-free clause $C$, every clause in $\Sigma'$ is also a ground 
instance of $C$.
Now it is easy to see that the same replacement of terms in the derivation of 
$E$ from $\Sigma$ results in a derivation of $E$ from $\Sigma'$:
(1) each resolution step in the derivation from $\Sigma$ can also be
carried out in the derivation from $\Sigma'$, since the same terms in 
$\Sigma$ are replaced by the same terms in $\Sigma'$, and (2) the terms
in $\Sigma$ that are not in $T$ (and hence are replaced by $t$) do not
appear in the conclusion $E$ of the derivation.

Since there is a derivation of $E$ from $\Sigma$ we have $\Sigma'\models E$, 
and hence $\Sigma'\models D\sigma$.
$\Sigma'$ is a set of ground instances of $C$ and all terms in $\Sigma'$ are 
terms in $T$, so $\Sigma'\subseteq{\cal I}(C,T)$.
Hence ${\cal I}(C,T)\models D\sigma$.
\end{proof}

\noindent Lemma~\ref{sufftermset} cannot be generalized to the case where 
$C$ contains function symbols of arity $\geq 1$, take 
$C=P(f(x),y)\leftarrow P(z,x)$ and $D=P(f(a),a)\leftarrow P(a,f(a))$
\cite<from the example given on p.~25 of>{id-almq93}. 
Then $T=\{a,f(a)\}$ is the term set of $D$ and we have $C\models D$, 
yet it can be seen that ${\cal I}(C,T)\not\models D$.
The argument used in the previous lemma does not work here, because different 
terms in some ground instance need not relate to different variables.
For example, in the ground instance $P(f^{2}(a),a)\leftarrow P(a,f(a))$ 
of $C$, we cannot just replace $f^{2}(a)$ by some other term, 
for then the resulting clause would not be an instance of $C$.

On the other hand, Lemma~\ref{sufftermset} can be generalized to
a {\em set} of clauses instead of a single clause.
If $\Sigma$ is a set of function-free clauses, $C$ is an arbitrary clause, 
and $\sigma$ is a Skolem substitution for $C$ w.r.t.\ $\Sigma$, then we have 
that $\Sigma\models C$ iff ${\cal I}(\Sigma,T)\models C\sigma$.
The proof is almost literally the same as above. 

This result implies that $\Sigma\models C$ is reducible to an implication 
${\cal I}(\Sigma,T)\models C\sigma$ between ground clauses.
Since, by the next lemma, implication between ground clauses is decidable,
it follows that $\Sigma\models C$ is decidable in case $\Sigma$ is 
function-free.

\begin{lemma}
The problem whether $\Sigma\models C$, where $\Sigma$ is a finite set of 
ground clauses and $C$ is a ground clause, is decidable.
\end{lemma}

\begin{proof}
Let $C=L_{1}\vee\ldots\vee L_{n}$ and $\cal A$ be the set of all ground
atoms occurring in $\Sigma$ and $C$. 
Now consider the following statements, which can be shown equivalent.\\
(1) $\Sigma\models C$.\\
(2) $\Sigma\cup\{\neg L_{1},\ldots,\neg L_{n}\}$ is unsatisfiable.\\ 
(3) $\Sigma\cup\{\neg L_{1},\ldots,\neg L_{n}\}$ has no Herbrand model.\\ 
(4) No subset of $\cal A$ is an Herbrand model of 
$\Sigma\cup\{\neg L_{1},\ldots,\neg L_{n}\}$.\\
Then (1)$\Leftrightarrow$(2). 
(2)$\Leftrightarrow$(3) by Theorem~4.2 of \cite{chang&lee73}.
Since also (3)$\Leftrightarrow$(4), we have (1)$\Leftrightarrow$(4).
(4) is decidable because $\cal A$ is finite, so (1) is decidable as well.
\end{proof}

\begin{corollary}\label{fnfreedec}
The problem whether $\Sigma\models C$, where $\Sigma$ is a finite set of 
function-free clauses and $C$ is a clause, is decidable.
\end{corollary}

\noindent The following sequence of lemmas more or less follows the
pattern of Idestam-Almquist's \citeyear{id-almq-jair} Lemma~10 to Lemma~12 
\cite<similar to Lemma 3.10 to Lemma 3.12 of>{id-almq93}.
There he gives a proof of the existence of a least generalization under 
T-implication of any finite set of (not necessarily function-free) clauses. 
We can adjust the proof in such a way that we can 
use it to establish the existence of an LGI of any finite set of clauses 
containing at least one non-tautologous function-free clause.

\begin{lemma}\label{finiteset}
Let $S$ be a finite set of non-tautologous clauses, $V=\{x_{1},\ldots,x_{m}\}$ 
be a set of variables and let $G=\{C_{1},C_{2}, \ldots\}$ be a (possibly 
infinite) set of generalizations of $S$ under implication.
Then the set $G'={\cal I}(C_{1},V)\cup{\cal I}(C_{2},V)\cup\ldots$ is
a finite set of clauses.
\end{lemma}

\begin{proof}
Let $d$ be the maximal depth of the terms in clauses in $S$.
It follows from Lemma~\ref{gottlob} that $G$ (and hence also $G'$) cannot 
contain terms of depth greater than $d$, nor predicates, functions or
constants other than those in $S$.
The set of literals which can be constructed from predicates in $S$
and from terms of depth at most $d$ consisting of functions and constants 
in $S$ and variables in $V$, is finite.
Hence the set of clauses which can be constructed from those literals is 
finite as well. 
$G'$ is a subset of this set, so $G'$ is a finite set of clauses.
\end{proof}

\begin{lemma}\label{lgthimplies}
Let $D$ be a clause, $C$ be a function-free clause such that $C\models D$,
$T=\{t_{1},\ldots,t_{n}\}$ be the term set of $D$ by $\sigma$, 
$V=\{x_{1},\ldots,x_{m}\}$ be a set of variables and $m\geq n$.
If $E$ is an LGS of ${\cal I}(C,V)$, then $E\models D$.
\end{lemma}

\begin{proof}
Let $\gamma=\{x_{1}/t_{1},\ldots,x_{n}/t_{n},x_{n+1}/t_{n},
\ldots,x_{m}/t_{n}\}$ (it does not matter to which terms the variables 
$x_{n+1},\ldots,x_{m}$ are mapped by $\gamma$, as long as they are mapped 
to terms in $T$).
Suppose ${\cal I}(C,V)=\{C\rho_{1},\ldots,C\rho_{k}\}$. 
Then ${\cal I}(C,T)=\{C\rho_{1}\gamma,\ldots,C\rho_{k}\gamma\}$.
Let $E$ be an LGS of ${\cal I}(C,V)$ (note that $E$ must be function-free).
Then for every $1\leq i\leq k$, there are $\theta_{i}$ such that 
$E\theta_{i}\subseteq C\rho_{i}$.
This means that $E\theta_{i}\gamma\subseteq C\rho_{i}\gamma$ and hence
$E\theta_{i}\gamma\models C\rho_{i}\gamma$, for every $1\leq i\leq k$.
Therefore $E\models{\cal I}(C,T)$.

Since $C\models D$, we know from Lemma~\ref{gottlob} that constants 
appearing in $C$ must also appear in $D$.
This means that $\sigma$ is a Skolem substitution for $D$ w.r.t.\ $\{C\}$.
Then from Lemma~\ref{sufftermset} we know ${\cal I}(C,T)\models D\sigma$,
hence $E\models D\sigma$. 
Furthermore, since $E$ is an LGS of ${\cal I}(C,V)$, all constants in $E$ 
also appear in $C$, hence all constants in $E$ must appear in $D$. 
Thus $\sigma$ is also a Skolem substitution for $D$ w.r.t.\ $\{E\}$.
Therefore $E\models D$ by Lemma~\ref{skolemimpl}.
\end{proof}

\noindent Consider $C=P(x,y,z)\leftarrow P(y,z,x)$ and $D=\leftarrow Q(w)$.
Both $C$ and $D$ imply the clause $E=P(x,y,z)\leftarrow P(z,x,y),Q(b)$. 
Now note that $C\cup D=P(x,y,z)\leftarrow P(y,z,x),Q(w)$ also implies $E$.
This holds for clauses in general, even in the presence of background 
knowledge $\Sigma$. The next lemma is very general, but in this section we 
only need the special case where $C$ and $D$ are function-free and $\Sigma$
is empty. We need the general case to prove the existence of a GSR in
Section~\ref{secgsr}.

\begin{lemma}\label{cupimpl}
Let $C$, $D$ and $E$ be clauses such that $C$ and $D$ are standardized apart
and let $\Sigma$ be a set of clauses.
If $C\models_{\Sigma}E$ and $D\models_{\Sigma}E$, then 
$C\cup D\models_{\Sigma}E$.
\end{lemma}

\begin{proof}
Suppose $C\models_{\Sigma}E$ and $D\models_{\Sigma}E$,
and let $M$ be a model of $\Sigma\cup\{C\cup D\}$.
Since $C$ and $D$ are standardized apart, the clause $C\cup D$ is equivalent
to the formula $\forall(C)\vee\forall(D)$ 
(where $\forall(C)$ denotes the universally quantified clause $C$).
This means that $M$ is a model of $C$ or a model of $D$.
Furthermore, $M$ is also a model of $\Sigma$, so it follows from 
$\Sigma\cup\{C\}\models E$ or $\Sigma\cup\{D\}\models E$ that $M$ is a 
model of $E$.
Thus $\Sigma\cup\{C\cup D\}\models E$, hence $C\cup D\models_{\Sigma}E$.
\end{proof}

\noindent Now we can prove the existence of an LGI of any finite set $S$ of 
clauses which contains at least one non-tautologous and function-free clause. 
In fact we can prove something stronger, namely that this LGI is a 
{\em special} LGI. This is an LGI that is not only implied, but actually
{\em subsumed} by any other generalization of $S$:

\begin{definition}
Let $\cal C$ be a clausal language and $S$ be a finite subset of $\cal C$.
An LGI $C$ of $S$ in $\cal C$ is called a {\em special} LGI of $S$ in
$\cal C$, if $C'\succeq C$ for every generalization $C'\in\cal C$ of $S$
under implication.
\end{definition}

\noindent Note that if $D$ is an LGI of a set containing at least one 
non-tautologous function-free clause, then by Lemma~\ref{gottlob} $D$ is 
itself function-free, because it should imply the function-free clause(s) 
in $S$. For instance, $C=P(x,y,z)\leftarrow P(y,z,x),Q(w)$ is an LGI of 
$D_{1}=P(x,y,z)\leftarrow P(y,z,x),Q(f(a))$ and 
$D_{2}=P(x,y,z)\leftarrow P(z,x,y),Q(b)$.
Note that this LGI is properly subsumed by the LGS of $\{D_{1},D_{2}\}$, 
which is $P(x,y,z)\leftarrow P(x',y',z'),Q(w)$.
An LGI may sometimes be the empty clause $\Box$, 
for example if $S=\{P(a), Q(a)\}$.

\begin{theorem}[Existence of special LGI in $\cal C$]\label{exlgi}
Let $\cal C$ be a clausal language.
If $S$ is a finite set of clauses from $\cal C$
and $S$ contains at least one non-tautologous function-free clause,
then there exists a special LGI of $S$ in $\cal C$.
\end{theorem}

\begin{proof}
Let $S=\{D_{1},\ldots,D_{n}\}$ be a finite set of clauses from $\cal C$, 
such that $S$ contains at least one non-tautologous function-free clause. 
We can assume without loss of generality that $S$ contains no tautologies.
Let $\sigma$ be a Skolem substitution for $S$, $T=\{t_{1},\ldots,
t_{m}\}$ be the term set of $S$ by $\sigma$, $V=\{x_{1},\ldots,x_{m}\}$ 
be a set of variables and $G=\{C_{1},C_{2},\ldots\}$ 
be the set of all generalizations of $S$ under implication in $\cal C$.
Note that $\Box\in G$, so $G$ is not empty.
Since each clause in $G$ must imply the function-free clause(s) in $S$, it 
follows from Lemma~\ref{gottlob} that all members of $G$ are function-free.
By Lemma~\ref{finiteset}, the set $G'={\cal I}(C_{1},V)\cup
{\cal I}(C_{2},V)\cup\ldots$ is a finite set of clauses.
Since $G'$ is finite, the set of ${\cal I}(C_{i},V)$s is also finite.
For simplicity, let $\{{\cal I}(C_{1},V),\ldots,{\cal I}(C_{k},V)\}$ be
the set of all distinct ${\cal I}(C_{i},V)$s. 

Let $E_{i}$ be an LGS of ${\cal I}(C_{i},V)$, for every $1\leq i\leq k$,
such that $E_{1},\ldots,E_{k}$ are standardized apart.
For every $1\leq j\leq n$, the term set of $D_{j}$ by $\sigma$ is some set 
$\{t_{j_{1}},\ldots,t_{j_{s}}\}\subseteq T$, such that $m\geq j_{s}$.
>From Lemma~\ref{lgthimplies}, we have that $E_{i}\models D_{j}$, for 
every $1\leq i\leq k$ and $1\leq j\leq n$, hence $E_{i}\models S$.
Now let $F=E_{1}\cup\ldots\cup E_{k}$, then
we have $F\models S$ from Lemma~\ref{cupimpl} (applying the case of
Lemma~\ref{cupimpl} where $\Sigma$ is empty).

To prove that $F$ is a special LGI of $S$, it remains to show that 
$C_{j}\succeq F$, for every $j\geq 1$.
For every $j\geq 1$, there is an $i$ ($1\leq i\leq k$),
such that ${\cal I}(C_{j},V)={\cal I}(C_{i},V)$.
So for this $i$, $E_{i}$ is an LGS of ${\cal I}(C_{j},V)$.
$C_{j}$ is itself also a generalization of ${\cal I}(C_{j},V)$ under
subsumption, hence $C_{j}\succeq E_{i}$.
Then finally $C_{j}\succeq F$, since $E_{i}\subseteq F$.
\end{proof}

\noindent As a consequence, we also immediately have the following:

\begin{corollary}[Existence of LGI for function-free clauses]\label{lggis}
Let $\cal C$ be a clausal language.
Then for every finite set of function-free clauses $S\subseteq\cal C$, 
there exists an LGI of $S$ in $\cal C$.
\end{corollary}

\begin{proof}
Let $S$ be a finite set of function-free clauses in $\cal C$.
If $S$ only contains tautologies, any tautology will be an LGI of $S$.
Otherwise, let $S'$ be obtained by deleting all tautologies from $S$.
By the previous theorem, there is a special LGI of $S'$.
Clearly, this is also a special LGI of $S$ itself in $\cal C$.
\end{proof}

\noindent This corollary is not trivial, since even though the number of 
Herbrand interpretations of a language without function symbols is finite 
(due to the fact that the number of all possible ground atoms is 
finite in this case), $S$ may nevertheless be implied by an infinite
number of non-equivalent clauses.
This may seem like a paradox, since there are only finitely many categories 
of clauses that can ``behave differently'' in a {\em finite} number of finite 
Herbrand interpretations. Thus it would seem that the number of non-equivalent function-free 
clauses should also be finite. This is a misunderstanding, since logical
implication (and hence also logical equivalence) is defined in terms of
{\em all} interpretations, not just Herbrand interpretations.
For instance, define $D_{1}=P(a,a)$ and $P(b,b)$, $C_{n}=\{P(x_{i},x_{j})
\mbox{ $|$ } i\neq j, 1\leq i,j\leq n\}$.
Then we have $C_{n}\models\{D_{1},D_{2}\}$, $C_{n}\models C_{n+1}$ and
$C_{n+1}\not\models C_{n}$, for every $n\geq 1$, see \cite{laag&cheng94}.

Another interesting consequence of Theorem~\ref{exlgi} concerns 
self-saturation (see the introduction to this paper for the definition
of self-saturation). 
If $C$ is a special LGI of some set $S$, then it is clear that $C$ is
self-saturated: any clause which implies $C$ also implies $S$ and hence
must {\em subsume} $C$, since $C$ is a special LGI of $S$.
Now consider $S=\{D\}$, where $D$ is some non-tautologous function-free 
clause. Then a special LGI $C$ of $S$ will be logically equivalent to $D$.
Moreover, since this $C$ will be self-saturated, it is a self-saturation
of $D$.

\begin{corollary}
If $D$ is a non-tautologous function-free clause, then there exists
a self-satura\-tion of $D$.
\end{corollary}





\subsection{The LGI is Computable}

In the previous subsection we proved the {\em existence} of an LGI in 
$\cal C$ of every finite set $S$ of clauses containing at least one 
non-tautologous function-free clause.
In this subsection we will establish the {\em computability} of such an LGI.
The next algorithm, extracted from the proof of the previous section, 
computes this LGI of $S$.

\vfill

\newpage

\begin{quote}
\noindent{\bf LGI-Algorithm}\\[3mm]
{\bf Input:} A finite set $S$ of clauses, containing at least one 
non-tautologous function-free clause.\\
{\bf Output:} An LGI of $S$ in $\cal C$.
\begin{shortenum}
\item Remove all tautologies from $S$ (a clause is a tautology iff it 
contains literals $A$ and $\neg A$), call the remaining set $S'$.
\item Let $m$ be the number of distinct terms (including subterms) in $S'$,
let $V=\{x_{1},\ldots,x_{m}\}$. (Notice that this $m$ is the same number
as the number of terms in the term set $T$ used in the proof of
Theorem~\ref{exlgi}.)
\item Let $G$ be the (finite) set of all clauses which can be constructed 
from predicates and constants in $S'$ and variables in $V$.
\item Let $\{U_{1},\ldots,U_{n}\}$ be the set of all subsets of $G$.
\item Let $H_{i}$ be an LGS of $U_{i}$, for every $1\leq i\leq n$.
These $H_{i}$ can be computed by Plotkin's \citeyear{plotkin1} algorithm.
\item Remove from $\{H_{1},\ldots,H_{n}\}$ all clauses which do not imply 
$S'$ (since each $H_{i}$ is function-free, by Corollary~\ref{fnfreedec}
this implication is decidable), 
and standardize the remaining clauses $\{H_{1},\ldots,H_{q}\}$ apart. 
\item Return the clause $H=H_{1}\cup\ldots\cup H_{q}$.
\end{shortenum}
\end{quote}

\noindent The correctness of this algorithm follows from the proof of 
Theorem~\ref{exlgi}. First notice that $H\models S$ by Lemma~\ref{cupimpl}.
Furthermore, note that all ${\cal I}(C_{i},V)$'s mentioned in the proof of 
Theorem~\ref{exlgi}, are elements of the set $\{U_{1},\ldots,U_{n}\}$. 
This means that for every $E_{i}$ in the set $\{E_{1},\ldots,E_{k}\}$
mentioned in that proof, there is a clause $H_{j}$ in $\{H_{1},\ldots,
H_{q}\}$ such that $E_{i}$ and $H_{j}$ are subsume-equivalent.
Then it follows that the LGI $F=E_{1}\cup\ldots\cup E_{k}$ of that proof 
subsumes the clause $H=H_{1}\cup\ldots\cup H_{q}$ that our algorithm returns.
On the other hand, $F$ is a special LGI, so $F$ and $H$ must be 
subsume-equivalent.

Suppose the number of distinct constants in $S'$ is $c$ and the 
number of distinct variables in step~2 of the algorithm is $m$. 
Furthermore, suppose there are $p$ distinct predicate symbols in $S'$,
with respective arities $a_{1},\ldots,a_{p}$.
Then the number of distinct atoms that can be formed from these constants,
variables and predicates, is $l=\sum_{i=1}^{p}(c+m)^{a_{i}}$,
and the number of distinct literals that can be formed is $2\cdot l$.
The set $G$ of distinct clauses which can be formed from these literals is 
the power set of this set of literals, so $|G|=2^{2\cdot l}$.
Then the set $\{U_{1},\ldots,U_{n}\}$ of all subsets of $G$ contains
$2^{|G|}=2^{2^{2\cdot l}}$ members.

Thus the algorithm outlined above is not very efficient (to say the least).
A more efficient algorithm may exist, but since implication is harder than
subsumption and the computation of an LGS is already quite expensive, we
should not put our hopes too high. 
Nevertheless, the existence of the LGI-algorithm does establish the 
theoretical point that the LGI of any finite set of clauses containing at 
least one non-tautologous function-free clause is effectively computable. 

\begin{theorem}[Computability of LGI]
Let $\cal C$ be a clausal language.
If $S$ is a finite set of clauses from $\cal C$,
and $S$ contains at least one non-tautologous function-free clause,
then the LGI of $S$ in $\cal C$ is computable.
\end{theorem}





\section{Greatest Specializations under Implication}\label{secgsi}

Now we turn from least generalizations under implication to 
greatest specializations.
Finding least generalizations of sets of clauses is common practice in ILP.
On the other hand, the greatest specialization, which is the dual of the 
least generalization, is used hardly ever.
Nevertheless, the GSI of two clauses $D_{1}$ and $D_{2}$ might be useful. 
Suppose that we have one positive example $e^{+}$ and two negative
examples $e^{-}_{1}$ and $e^{-}_{2}$ and suppose that $D_{1}$ implies
$e^{+}$ and $e^{-}_{1}$, while $D_{2}$ implies $e^{+}$ and $e^{-}_{2}$. 
Then it might very well be that the GSI of $D_{1}$ and $D_{2}$ still 
implies $e^{+}$, but does not imply either $e^{-}_{1}$ or $e^{-}_{2}$.
Thus we could obtain a correct specialization by taking the GSI of $D_{1}$
and $D_{2}$.

It is obvious from the previous sections that the existence of an 
LGI of $S$ is quite hard to establish.
For clauses which all contain functions, the existence of an LGI is still 
an open question, and even for the case where $S$ contains at least one 
non-tautologous function-free clause, the proof was far from trivial.
However, the existence of a GSI in $\cal C$ is much easier to prove.
In fact, a GSI of a finite set $S$ is the same as the GSS of $S$, namely 
the union of the clauses in $S$ after these are standardized apart.

To see the reason for this dissymmetry, let us take a step back from the 
clausal framework and consider full first-order logic for a moment.
If $\phi_{1}$ and $\phi_{2}$ are two arbitrary first-order formulas,
then it can be easily shown that their least generalization is just
$\phi_{1}\wedge\phi_{2}$: this conjunction implies $\phi_{1}$ and $\phi_{1}$, 
and must be implied by any other formula which implies both $\phi_{1}$ and 
$\phi_{2}$. 
Dually, the greatest specialization is just $\phi_{1}\vee\phi_{2}$: this 
is implied by both $\phi_{1}$ and $\phi_{2}$, and must imply any other 
formula that is implied by both $\phi_{1}$ and $\phi_{2}$. 
See figure~\ref{folgigsi}.

\begin{figure}[hbt]
\centering
\setlength{\unitlength}{0.2mm}
\begin{picture}(120,140)
{\scriptsize

\put(0,0){
\begin{picture}(120,130)
\put(70,130){\makebox(0,0){$\phi_{1}\wedge\phi_{2}$}}
\put(60,120){\vector(-1,-1){50}}
\put(80,120){\vector(1,-1){50}}

\put(0,65){\makebox(0,0){$\phi_{1}$}}
\put(140,65){\makebox(0,0){$\phi_{2}$}}
\put(10,60){\vector(1,-1){50}}
\put(130,60){\vector(-1,-1){50}}

\put(70,0){\makebox(0,0){$\phi_{1}\vee\phi_{2}$}}
\end{picture}}
}
\end{picture}
\caption{Least generalization and greatest specialization in first-order logic}
\label{folgigsi}
\end{figure}

Now suppose $\phi_{1}$ and $\phi_{2}$ are clauses. Then why do we have a 
problem in finding the LGI of $\phi_{1}$ and $\phi_{2}$?
The reason for this is that $\phi_{1}\wedge\phi_{2}$ is not a clause.
Instead of using $\phi_{1}\wedge\phi_{2}$, we have to find some least
clause which implies both clauses $\phi_{1}$ and $\phi_{2}$.
Such a clause appears quite hard to find sometimes.

On the other hand, in case of specialization there is no problem.
Here we can take $\phi_{1}\vee\phi_{2}$ as GSI, since $\phi_{1}\vee\phi_{2}$
is equivalent to a clause, if we handle the universal quantifiers in front
of a clause properly. If $\phi_{1}$ and $\phi_{2}$ are standardized apart, 
then the formula $\phi_{1}\vee\phi_{2}$ is equivalent to the 
clause which is the union of $\phi_{1}$ and $\phi_{2}$. 
This fact was used in the proof of Lemma~\ref{cupimpl}.

Suppose $S=\{D_{1},\ldots,D_{n}\}$, and $D'_{1},\ldots,D'_{n}$ are variants 
of these clauses which are standardized apart.
Then clearly $D=D'_{1}\cup\ldots\cup D'_{n}$ is a GSI of $S$,
since it follows from Lemma~\ref{cupimpl} that any specialization of $S$
under implication is implied by $D$. Thus we have the following result:

\begin{theorem}[Existence of GSI in ${\cal C}$]
Let $\cal C$ be a clausal language.
Then for every finite $S\subseteq\cal C$, there exists a GSI of $S$
in $\cal C$.
\end{theorem}

\noindent 
The previous theorem holds for clauses in general, so in particular also
for function-free clauses. Furthermore, Corollary~\ref{lggis} guarantees us
that in a function-free clausal language an LGI of every finite $S$ exists.
This means that the set of function-free clauses quasi-ordered by logical
implication is in fact a lattice.

\begin{corollary}[Lattice-structure of function-free clauses under $\models$]\hspace*{0.3mm}
A function-free clausal language ordered by implication is a lattice.
\end{corollary}

\noindent In case of a Horn language $\cal H$, we cannot apply the same
proof method as in the case of a clausal language, since the union of
two Horn clauses need not be a Horn clause itself.
In fact, we can show that not every finite set of Horn clauses has a GSI 
in $\cal H$. Here we can use the same clauses that we used to show that 
sets of Horn clauses need not have an LGI in $\cal H$, this time from the
perspective of specialization instead of generalization.

Again, let $D_{1}=P(f^{2}(x))\leftarrow P(x)$, $D_{2}=P(f^{3}(x))\leftarrow 
P(x)$, $C_{1}=P(f(x))\leftarrow P(x)$ and $C_{2}=P(f^{2}(y))\leftarrow P(x)$.
Then $C_{1}\models\{D_{1},D_{2}\}$ and $C_{2}\models\{D_{1},D_{2}\}$,
and there is no Horn clause $D$ such that $D\models D_{1}$, $D\models D_{2}$, 
$C_{1}\models D$ and $C_{2}\models D$.
Hence there is no GSI of $\{C_{1},C_{2}\}$ in $\cal H$.





\section{Least Generalizations under Relative Implication}\label{seclgr}

Implication is stronger than subsumption, but {\em relative}
implication is even more powerful, because background knowledge can
be used to model all sorts of useful properties and relations.
In this section, we will discuss least generalizations under implication
relative to some given background knowledge $\Sigma$ (LGR's).
In the next section we treat greatest specializations under relative
implication.

First, we will prove the equivalence between our definition of relative
implication and a definition given by \fullciteA[p.~133]{niblett}.
He gives the following definition of subsumption
relative to a background knowledge $\Sigma$ (to distinguish it
from our notion of subsumption, we will call this `N-subsumption'):%
\footnote{Niblett attributes this definition to Plotkin, though Plotkin 
gives a rather different definition of relative subsumption in~\cite{plotkin2}, 
as we have seen in Section~\ref{secsubs}.}

\begin{definition}
Clause $C$ {\em N-subsumes} clause $D$ with respect to background knowledge 
$\Sigma$ if there is a substitution $\theta$ such that 
$\Sigma\vdash(C\theta\rightarrow D)$ 
(here `$\rightarrow$' is the implication-connective,
and `$\vdash$' is an arbitrary complete proof procedure). 
\end{definition}

\begin{proposition}
Let $C$ and $D$ be clauses and $\Sigma$ be a set of clauses.
Then $C$ N-subsumes $D$ with respect to $\Sigma$ iff $C\models_{\Sigma}D$.
\end{proposition}

\begin{proof}
Consider the following six statements, which can be shown equivalent.\\
(1) $C$ N-subsumes $D$ with respect to $\Sigma$.\\
(2) There is a substitution $\theta$ such that $\Sigma\vdash  (C\theta\rightarrow D)$.\\ 
(3) There is a substitution $\theta$ such that $\Sigma\models (C\theta\rightarrow D)$.\\
(4) There is a substitution $\theta$ such that $\Sigma\cup\{C\theta\}\models D$.\\
(5) $\Sigma\cup\{C\}\models D$.\\
(6) $C\models_{\Sigma}D$.\\
(1)$\Leftrightarrow$(2) by definition. 
(2)$\Leftrightarrow$(3) by the completeness of $\vdash$.
(3)$\Leftrightarrow$(4) by the Deduction Theorem.
(4)$\Rightarrow$(5) is obvious and (5)$\Rightarrow$(4) follows from 
letting $\theta$ be the empty substitution, hence (4)$\Leftrightarrow$(5).
Finally, (5)$\Leftrightarrow$(6) by definition.
Thus these six statements are equivalent.
\end{proof}

\noindent Since $\models$ is the special case of $\models_{\Sigma}$ where 
$\Sigma$ is empty, our counterexamples to the existence of LGI's or GSI's 
in ${\cal H}$ are also counterexamples to the existence of LGR's or GSR's 
in ${\cal H}$.
In other words, the `$-$'-entries in the second row of Table~\ref{lggstable}
carry over to the third row.

For general clauses, the LGR-question also has a negative answer.
We will show here that even if $S$ and $\Sigma$ are both finite sets of 
{\em function-free} clauses, an LGR of $S$ relative to $\Sigma$ need not 
exist. Let $D_{1}=P(a)$, $D_{2}=P(b)$, $S=\{D_{1},D_{2}\}$,
and $\Sigma=\{(P(a)\vee\neg Q(x)), (P(b)\vee\neg Q(x))\}$.
We will show that this $S$ has no LGR relative to $\Sigma$ in $\cal C$.

Suppose $C$ is an LGR of $S$ relative to $\Sigma$.
Note that if $C$ contains the literal $P(a)$, then the Herbrand 
interpretation which makes $P(a)$ true and which makes all other ground 
literals false, would be a model of $\Sigma\cup\{C\}$ but not of $D_{2}$, 
so then we would have $C\not\models_{\Sigma}D_{2}$.
Similarly, if $C$ contains $P(b)$ then $C\not\models_{\Sigma}D_{1}$.
Hence $C$ cannot contain $P(a)$ or $P(b)$.

Now let $d$ be a constant not appearing in $C$.
Let $D=P(x)\vee Q(d)$, then $D\models_{\Sigma}S$.
By the definition of an LGR, we should have $D\models_{\Sigma}C$.
Then by the subsumption theorem, there must be a derivation from 
$\Sigma\cup\{D\}$ of a clause $E$, which subsumes $C$. 
The set of all clauses which can be derived (in 0 or more resolution-steps) 
from $\Sigma\cup\{D\}$ is $\Sigma\cup\{D\}\cup\{(P(a)\vee P(x)),
(P(b)\vee P(x))\}$.
But none of these clauses subsumes $C$, because $C$ does not contain 
the constant $d$, nor the literals $P(a)$ or $P(b)$.
Hence $D\not\models_{\Sigma}C$, contradicting the assumption that
$C$ is an LGR of $S$ relative to $\Sigma$ in $\cal C$.

Thus in general the LGR of $S$ relative to $\Sigma$ need not exist. 
However, we can identify a special case in which the LGR {\em does} exist. 
This case might be of practical interest.
Suppose $\Sigma=\{L_{1},\ldots,L_{m}\}$ is a finite set of 
{\em function-free ground} literals. 
We can assume $\Sigma$ does not contain complementary literals 
(i.e., $A$ and $\neg A$), for otherwise $\Sigma$ would be inconsistent.
Also, suppose $S=\{D_{1},\ldots,D_{n}\}$ is a set of clauses,
at least one of which is non-tautologous and function-free.
Then $C\models_{\Sigma}D_{i}$ iff $\{C\}\cup\Sigma\models D_{i}$
iff $C\models D_{i}\vee\neg(L_{1}\wedge\ldots\wedge L_{m})$ iff 
$C\models D_{i}\vee\neg L_{1}\vee\ldots\vee\neg L_{m}$. This means that an 
LGI of the set of clauses $\{(D_{1}\vee\neg L_{1}\vee\ldots\vee\neg L_{m}),
\ldots,(D_{n}\vee\neg L_{1}\vee\ldots\vee\neg L_{m})\}$ is also an LGR of
$S$ relative to $\Sigma$.
If some $D_{k}\vee\neg L_{1}\vee\ldots\vee\neg L_{m}$ is non-tautologous
and function-free, this LGI exists and is computable.
Hence in this special case, the LGR of $S$ relative to $\Sigma$ exists and
is computable.







\section{Greatest Specializations under Relative Implication}\label{secgsr}

Since the counterexample to the existence of GSI's in ${\cal H}$ is also a 
counterexample to the existence of GSR's in ${\cal H}$, the only remaining 
question in the $\models_{\Sigma}$-order is the existence of GSR's in 
${\cal C}$. The answer to this question is positive.
In fact, like the GSS and the GSI, the GSR of some finite set $S$ in $\cal C$
is just the union of the (standardized apart) clauses in $S$.

\begin{theorem}[Existence of GSR in ${\cal C}$]
Let $\cal C$ be a clausal language and $\Sigma\subseteq\cal C$.
Then for every finite $S\subseteq\cal C$, there exists a GSR of $S$
relative to $\Sigma$ in $\cal C$.
\end{theorem}

\begin{proof}
Suppose $S=\{D_{1},\ldots,D_{n}\}\subseteq\cal C$. Without loss of 
generality, we assume the clauses in $S$ are standardized apart.
Let $D=D_{1}\cup\ldots\cup D_{n}$, then $D_{i}\models_{\Sigma}D$, 
for every $1\leq i\leq n$. Now let $C\in\cal C$ be such that 
$D_{i}\models_{\Sigma}C$, for every $1\leq i\leq n$.
Then from Lemma~\ref{cupimpl}, we have $D\models_{\Sigma}C$. 
Hence $D$ is a GSR of $S$ relative to $\Sigma$ in $\cal C$.
\end{proof}






\section{Conclusion}

In ILP, the three main generality orders are subsumption, implication, 
and relative implication. 
The two main languages are clausal languages and Horn languages.
This gives a total of six different ordered sets.
In this paper, we have given a systematic treatment of the existence
or non-existence of least generalizations and greatest specializations
in each of these six ordered sets.
The outcome of this investigation is summarized in Table~\ref{lggstable}.
The only remaining open question is the existence or non-existence of a least 
generalization under implication in $\cal C$ for sets of clauses which all 
contain function symbols.

Table~\ref{lggstable} makes explicit the trade-off between different
generality orders. On the one hand, implication is better suited as a
generality order than subsumption, particularly in case of recursive clauses.
Relative implication is still better, because it allows us to take background
knowledge into account.
On the other hand, we can see from the table that as far as the existence
of least generalizations goes, subsumption is more attractive than
logical implication, and logical implication is in turn more attractive
than relative implication.
For subsumption, least generalizations always exist. 
For logical implication, we can only prove the existence of least 
generalizations in the presence of a function-free clause. 
And finally, for relative implication, least generalizations need 
not even exist in a function-free language.
In practice this means that we cannot have it all. 
If we choose to use a very strong generality order such as relative 
implication, least generalizations only exist in very limited cases.
On the other hand, if we want to guarantee that least generalizations
always exist, we are committed to the weakest generality order: subsumption.


\acks{We would like to thank Peter Idestam-Almquist and the referees
for their comments, which helped to improve the paper.}



\vskip 0.2in
%\bibliography{ilpbib}
\bibliographystyle{theapa}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Aha}{Aha}{1992}]{aha}
Aha, D.~W. \BBOP1992\BBCP.
\newblock \BBOQ Relating relational learning algorithms\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Inductive Logic Programming},
  \lowercase{\BVOL}~38 of {\Bem APIC Series}, \BPGS\ 233--254. Academic Press.

\bibitem[\protect\BCAY{Chang \BBA\ Lee}{Chang \BBA\ Lee}{1973}]{chang&lee73}
Chang, C.-L.\BBACOMMA\  \BBA\ Lee, R. C.-T. \BBOP1973\BBCP.
\newblock {\Bem Symbolic Logic and Mechanical Theorem Proving}.
\newblock Academic Press, San Diego.

\bibitem[\protect\BCAY{De~Raedt \BBA\ Bruynooghe}{De~Raedt \BBA\
  Bruynooghe}{1993}]{deraedt&bruynooghe}
De~Raedt, L.\BBACOMMA\  \BBA\ Bruynooghe, M. \BBOP1993\BBCP.
\newblock \BBOQ A theory of clausal discovery\BBCQ\
\newblock In {\Bem Proceedings of the 13th International Joint Conference
  on Artificial Intelligence (IJCAI-93)}, \BPGS\ 1058--1063. Morgan Kaufmann.

\bibitem[\protect\BCAY{Gottlob}{Gottlob}{1987}]{gottlob}
Gottlob, G. \BBOP1987\BBCP.
\newblock \BBOQ Subsumption and implication\BBCQ\
\newblock {\Bem Information Processing Letters}, {\Bem 24\/}(2), 109--111.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1993}]{id-almq93}
Idestam-Almquist, P. \BBOP1993\BBCP.
\newblock {\Bem Generalization of Clauses}.
\newblock Ph.D.\ thesis, Stockholm University.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1995}]{id-almq-jair}
Idestam-Almquist, P. \BBOP1995\BBCP.
\newblock \BBOQ Generalization of clauses under implication\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 3},
  467--489.

\bibitem[\protect\BCAY{Kowalski}{Kowalski}{1970}]{kowalski}
Kowalski, R.~A. \BBOP1970\BBCP.
\newblock \BBOQ The case for using equality axioms in automatic
  demonstration\BBCQ\
\newblock In {\Bem Proceedings of the Symposium on Automatic Demonstration},
  \lowercase{\BVOL}\ 125 of {\Bem Lecture Notes in Mathematics}, \BPGS\
  112--127. Springer-Verlag.

\bibitem[\protect\BCAY{Lavra{\v{c}} \BBA\ D{\v{z}}eroski}{Lavra{\v{c}} \BBA\
  D{\v{z}}eroski}{1994}]{lavrac&dzeroski94}
Lavra{\v{c}}, N.\BBACOMMA\  \BBA\ D{\v{z}}eroski, S. \BBOP1994\BBCP.
\newblock {\Bem Inductive Logic Programming: Techniques and Applications}.
\newblock Ellis Horwood.

\bibitem[\protect\BCAY{Lee}{Lee}{1967}]{lee67}
Lee, R. C.-T. \BBOP1967\BBCP.
\newblock {\Bem A Completeness Theorem and a Computer Program for Finding
  Theorems Derivable from Given Axioms}.
\newblock Ph.D.\ thesis, University of California, Berkeley.

\bibitem[\protect\BCAY{Lloyd}{Lloyd}{1987}]{lloyd87}
Lloyd, J.~W. \BBOP1987\BBCP.
\newblock {\Bem Foundations of Logic Programming\/} (Second \BEd).
\newblock Springer-Verlag, Berlin.

\bibitem[\protect\BCAY{Marcinkowski \BBA\ Pacholski}{Marcinkowski \BBA\
  Pacholski}{1992}]{marc&pach}
Marcinkowski, J.\BBACOMMA\  \BBA\ Pacholski, L. \BBOP1992\BBCP.
\newblock \BBOQ Undecidability of the horn-clause implication problem\BBCQ\
\newblock In {\Bem Proceedings of the 33rd Annual IEEE Symposium on Foundations
  of Computer Science}, \BPGS\ 354--362\ Pittsburg.

\bibitem[\protect\BCAY{Morik, Wrobel, Kietz, \BBA\ Emde}{Morik
  et~al.}{1993}]{morikea:mobal}
Morik, K., Wrobel, S., Kietz, J.-U., \BBA\ Emde, W. \BBOP1993\BBCP.
\newblock {\Bem Knowledge Acquisition and Machine Learning: Theory, Methods and
  Applications}.
\newblock Academic Press, London.

\bibitem[\protect\BCAY{Muggleton}{Muggleton}{1992}]{muggleton-ilp}
Muggleton, S. \BBOP1992\BBCP.
\newblock \BBOQ Inductive logic programming\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Inductive Logic Programming},
  \lowercase{\BVOL}~38 of {\Bem APIC Series}, \BPGS\ 3--27. Academic Press.

\bibitem[\protect\BCAY{Muggleton \BBA\ De~Raedt}{Muggleton \BBA\
  De~Raedt}{1994}]{muggleton&deraedt}
Muggleton, S.\BBACOMMA\  \BBA\ De~Raedt, L. \BBOP1994\BBCP.
\newblock \BBOQ Inductive logic programming: Theory and methods\BBCQ\
\newblock {\Bem Journal of Logic Programming}, {\Bem 19}, 629--679.

\bibitem[\protect\BCAY{Muggleton \BBA\ Feng}{Muggleton \BBA\
  Feng}{1992}]{muggleton-golem}
Muggleton, S.\BBACOMMA\  \BBA\ Feng, C. \BBOP1992\BBCP.
\newblock \BBOQ Efficient induction of logic programs\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Inductive Logic Programming},
  \lowercase{\BVOL}~38 of {\Bem APIC Series}, \BPGS\ 281--298. Academic Press.

\bibitem[\protect\BCAY{Muggleton \BBA\ Page}{Muggleton \BBA\
  Page}{1994}]{muggleton-selfsat}
Muggleton, S.\BBACOMMA\  \BBA\ Page, C.~D. \BBOP1994\BBCP.
\newblock \BBOQ Self-saturation of definite clauses\BBCQ\
\newblock In Wrobel, S.\BED, {\Bem Proceedings of the 4th International
  Workshop on Inductive Logic Programming (ILP-94)}, \lowercase{\BVOL}\ 237 of
  {\Bem GMD-Studien}, \BPGS\ 161--174\ Bad Honnef/Bonn. Gesellschaft f{\"{u}}r
  Mathematik und Datenverarbeitung.

\bibitem[\protect\BCAY{Niblett}{Niblett}{1988}]{niblett}
Niblett, T. \BBOP1988\BBCP.
\newblock \BBOQ A study of generalisation in logic programs\BBCQ\
\newblock In Sleeman, D.\BED, {\Bem Proceedings of the 3rd European Working
  Sessions on Learning (EWSL-88)}, \BPGS\ 131--138.

\bibitem[\protect\BCAY{Nienhuys-Cheng \BBA\ de~Wolf}{Nienhuys-Cheng \BBA\
  de~Wolf}{1996}]{cheng&wolf:f&f}
Nienhuys-Cheng, S.-H.\BBACOMMA\  \BBA\ de~Wolf, R. \BBOP1996\BBCP.
\newblock \BBOQ The subsumption theorem in inductive logic programming: Facts
  and fallacies\BBCQ\
\newblock In De~Raedt, L.\BED, {\Bem Advances in Inductive Logic Programming},
  \BPGS\ 265--276\ Amsterdam. IOS Press.

\bibitem[\protect\BCAY{Plotkin}{Plotkin}{1970}]{plotkin1}
Plotkin, G.~D. \BBOP1970\BBCP.
\newblock \BBOQ A note on inductive generalization\BBCQ\
\newblock {\Bem Machine Intelligence}, {\Bem 5}, 153--163.

\bibitem[\protect\BCAY{Plotkin}{Plotkin}{1971a}]{plotkin:phd}
Plotkin, G.~D. \BBOP1971a\BBCP.
\newblock {\Bem Automatic Methods of Inductive Inference}.
\newblock Ph.D.\ thesis, Edinburgh University.

\bibitem[\protect\BCAY{Plotkin}{Plotkin}{1971b}]{plotkin2}
Plotkin, G.~D. \BBOP1971b\BBCP.
\newblock \BBOQ A further note on inductive generalization\BBCQ\
\newblock {\Bem Machine Intelligence}, {\Bem 6}, 101--124.

\bibitem[\protect\BCAY{Quinlan \BBA\ Cameron-Jones}{Quinlan \BBA\
  Cameron-Jones}{1993}]{foil}
Quinlan, J.~R.\BBACOMMA\  \BBA\ Cameron-Jones, R.~M. \BBOP1993\BBCP.
\newblock \BBOQ Foil: A midterm report\BBCQ\
\newblock In Brazdil, P.\BED, {\Bem Proceedings of the 6th European Conference
  on Machine Learning (ECML-93)}, \lowercase{\BVOL}\ 667 of {\Bem Lecture Notes
  in Artificial Intelligence}, \BPGS\ 3--20. Springer-Verlag.

\bibitem[\protect\BCAY{Reynolds}{Reynolds}{1970}]{reynolds}
Reynolds, J.~C. \BBOP1970\BBCP.
\newblock \BBOQ Transformational systems and the algebraic structure of atomic
  formulas\BBCQ\
\newblock {\Bem Machine Intelligence}, {\Bem 5}, 135--151.

\bibitem[\protect\BCAY{Rouveirol}{Rouveirol}{1992}]{rouveirol}
Rouveirol, C. \BBOP1992\BBCP.
\newblock \BBOQ Extensions of inversion of resolution applied to theory
  completion\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Inductive Logic Programming},
  \lowercase{\BVOL}~38 of {\Bem APIC Series}, \BPGS\ 63--92. Academic Press.

\bibitem[\protect\BCAY{Shapiro}{Shapiro}{1981}]{shapiro81}
Shapiro, E.~Y. \BBOP1981\BBCP.
\newblock \BBOQ Inductive inference of theories from facts\BBCQ\
\newblock Research report\ 192, Yale University.

\bibitem[\protect\BCAY{van~der Laag \BBA\ Nienhuys-Cheng}{van~der Laag \BBA\
  Nienhuys-Cheng}{1994}]{laag&cheng94}
van~der Laag, P. R.~J.\BBACOMMA\  \BBA\ Nienhuys-Cheng, S.-H. \BBOP1994\BBCP.
\newblock \BBOQ Existence and nonexistence of complete refinement
  operators\BBCQ\
\newblock In Bergadano, F.\BBACOMMA\  \BBA\ De~Raedt, L.\BEDS, {\Bem
  Proceedings of the 7th European Conference on Machine Learning (ECML-94)},
  \lowercase{\BVOL}\ 784 of {\Bem Lecture Notes in Artificial Intelligence},
  \BPGS\ 307--322. Springer-Verlag.

\end{thebibliography}


\end{document}



