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

\jairheading{3}{1995}{467-489}{5/95}{12/95}
\ShortHeadings{Generalization of Clauses under Implication}
{Idestam-Almquist}
\firstpageno{467}

\begin{document}

\title{Generalization of Clauses under Implication}

\author{\name Peter Idestam-Almquist \email pi@dsv.su.se \\
       \addr Department of Computer and Systems Sciences, 
	Stockholm University \\
	Electrum 230, S-164 40 Kista, Sweden}

\maketitle


\newenvironment{definition}{
	\begin{list}{}{\setlength{\leftmargin}{0pt}}\item {\bf Definition}}{
	\end{list}}

\newenvironment{example}{
	\begin{list}{}{\setlength{\leftmargin}{0pt}}\item {\bf Example}}{
	\end{list}}

\newenvironment{proof}{
	\begin{list}{}{\setlength{\leftmargin}{0pt}}\item {\bf Proof:}}{
	$\Box$\end{list}}

\newenvironment{tab}{
	\tt\begin{tabbing}\makebox[35pt][l]{ }\=\\*}{
	\end{tabbing}}

\newtheorem{theorem}{Theorem}

\newtheorem{proposition}[theorem]{Proposition}

\newtheorem{lemma}[theorem]{Lemma}

\newtheorem{corollary}[theorem]{Corollary}


\hyphenation{-sub-sump-tion}
\hyphenation{sub-sump-tion}


\maketitle



\begin{abstract}
In the area of inductive learning, generalization is a main operation, and 
the usual definition of induction is based on logical implication. 
Recently there has been a rising interest in clausal representation of 
knowledge in machine learning. Almost all inductive learning systems 
that perform generalization of clauses use the relation 
$\theta$-subsumption instead of implication. The main reason is that there 
is a well-known and simple technique to compute least general generalizations 
under $\theta$-subsumption, but not under implication. 
However generalization under $\theta$-sub\-sumption is inappropriate 
for learning recursive clauses, which is a crucial problem since recursion is 
the basic program structure of logic programs. 

We note that implication between clauses is undecidable, and 
we therefore introduce a stronger form of implication, called T-implication, 
which is decidable between clauses. 
We show that for every finite set of clauses there exists a least general 
generalization under T-implication. 
We describe a technique to reduce generalizations under implication 
of a clause to generalizations under $\theta$-subsumption of what we call an 
expansion of the original clause. Moreover we show that for every non-tautological 
clause there exists a T-complete expansion, which means that every generalization 
under T-implication of the clause is reduced to a generalization under 
$\theta$-subsumption of the expansion. 
\end{abstract}

% \newpage




\section{Introduction}
\label{cIn}

The topic of this paper is generalization of clauses, which is a 
central problem in the area of Inductive Logic Programming (ILP) 
\cite{Mug91,Mug93}. ILP can be seen as the intersection of inductive 
machine learning and computational logic. In inductive machine learning 
the goal is to develop techniques for inducing hypotheses from 
examples (observations). By using the rich representation formalism 
of computational logic (clauses) for hypotheses and examples, 
ILP can overcome the limitations of classical machine learning 
representations, such as decision trees \cite{Qui86}. 

By using a clausal representation we have the ability to learn all 
types of hypotheses describable in first-order logic, in particular 
the important class of recursive hypotheses. Another advantage of 
using a clausal representation is that clausal theories are easy 
to manipulate for machine learning algorithms. This is due to that 
changes to a clausal theory by adding or deleting clauses or literals 
have clear and simple effects on the generality of the theory. 
The reader is referred to two introductions to ILP, one presented by 
Muggleton and De Raedt \nocite{MD94}(1994), and one by Lavra\v{c} and 
D\v{z}eroski \nocite{LD94}(1994). Lavra\v{c} and De Raedt 
\nocite{LD95}(1995) present a recent survey of ILP research.

% Generalization is a main operation in inductive machine learning. 
We use the following definition of induction. A theory (background knowledge) 
$T$, a set of positive examples $\{E_{1}^{+},\ldots,E_{n}^{+}\}$ and 
a set of negative examples $\{E_{1}^{-},\ldots,E_{m}^{-}\}$ of a target 
concept are given. 
Then a hypothesis $H$ for the target concept is an 
{\em inductive conclusion}\index{inductive conclusion} 
if and only if:
\begin{itemize}
\item[1)] $T\not\models E_{1}^{+}\wedge\ldots\wedge E_{n}^{+}$,
\item[2)] $T\wedge H\models E_{1}^{+}\wedge\ldots\wedge E_{n}^{+}$, and 
\item[3)] $T\wedge H\not\models E_{1}^{-}\vee\ldots\vee E_{m}^{-}$.
\end{itemize}
In other words, the positive examples should not be a logical consequence 
of the theory alone, but a logical consequence of the theory together with 
the hypothesis, 
and no negative example should be a logical consequence of the theory and 
the hypothesis.
Using clausal representation $T$, $H$, $\{E_{1}^{+},\ldots,E_{n}^{+}\}$ and 
$\{E_{1}^{-},\ldots,E_{m}^{-}\}$ are sets of clauses. 

In this paper we concentrate on the subproblem in inductive learning of 
finding a clause that is a generalization of a set of positive examples. 
In other words, finding a clause $C$ such that 
\[ C\models E_{1}^{+}\wedge\ldots\wedge E_{n}^{+}.\]
We are particularly interested in least general generalizations, 
since every generalization of a set of clauses is also a generalization 
of the least general generalization of this set of clauses. 
Therefore a least general generalization in some sense represents 
all generalizations. 
A least general generalization is also consistent with the negative 
examples whenever there exists a consistent generalization. 

The most natural and straightforward basis for generalization is implication, 
since induction is defined in terms of logical consequence. 
Plotkin has described \nocite{Plo70,Plo71b}(1970, 1971a) a technique for the 
computation of least general generalizations of clauses under a relation called 
$\theta$-subsumption. This relation has been accorded 
much interest, and it is often used instead of implication, since it is easier 
to compute. However, there is a difference between $\theta$-subsumption and 
implication, which sometimes causes the generalizations obtained by Plotkin's 
technique to be over-generalizations with respect to implication.

Consider the following clauses in which $s$ denotes the successor 
function:
\[\begin{array}{l}
C_{1}=(\:number(s(0))\leftarrow number(0)\:),\\ 
C_{2}=(\:number(s^{3}(0))\leftarrow number(s(0))\:),\\ 
D_{1}=(\:number(s(x))\leftarrow number(y)\:),$ and $\\ 
D_{2}=(\:number(s(x))\leftarrow number(x)\:).
\end{array} \]
The clause $D_{1}$ is a least general generalization under $\theta$-subsumption 
(LGG$\theta$) of $C_{1}$ and $C_{2}$, and the clause $D_{2}$ is a least general 
generalization under implication (LGGI) of $C_{1}$ and $C_{2}$. It is clear that 
$D_{1}$ is strictly more general than $D_{2}$, both under $\theta$-subsumption 
and under implication. It is also clear that $D_{2}$ is more appropriate in a 
definition of natural number.

To learn recursive clauses, generalization under $\theta$-subsumption is 
not very adequate, as illustrated above. The ability to learn recursive 
clauses is crucial, since recursion is the basic program structure of 
logic programs. 

In section \ref{GoC}, we describe the most important results 
concerning generalization under $\theta$-subsumption, and present 
a theoretically study of generalization under implication. 
In section \ref{RoItts}, we present a technique to reduce 
implication to $\theta$-subsumption based on or-introduction of 
literals. Finally, our results, computational complexity and future work 
are discussed in section \ref{CR}.

We assume the reader to be familiar with the basic notions and notations 
in Logic Programming \cite{Llo87} and/or Automatic Theorem Proving 
\cite{CL73,Gal86}. 




\section{Generalization of Clauses}
\label{GoC}

In the area of Inductive Logic Programming (ILP), the framework 
for generalization of clauses developed by Plotkin 
\nocite{Plo70,Plo71,Plo71b}(1970, 1971b, 1971a), has been accorded 
much interest. In this section we will describe this framework, which 
is based on a relation known as $\theta$-subsumption, and the most 
important results connected with it. 

Since generalization under $\theta$-subsumption is not 
sufficient for generalization of recursive clauses, as shown 
in the introduction, we will study the theory of generalization 
under implication. We note that implicaton between clauses is 
undecidable, and we will therefore introduce a restricted form 
of implication, called T-implication.



\subsection{Generalization under $\theta$-subsumption}

% We first give the definition of $\theta$-subsumption. 

\begin{definition}
A clause $C$ 
{\em $\theta$-subsumes}\index{
$\theta$-subsumes}\index{theta-subsumes} a clause $D$, 
denoted $C\preceq D$\index{$\preceq$ ($\theta$-subsumes)}, 
if and only if 
there exists a substitution $\theta$ such that $C\theta\subseteq D$. 
% We say that $C$ is a {\em $\theta$-subsumer} of $D$.  
Two clauses $C$ and $D$ are 
{\em equivalent under $\theta$-subsump\-tion}\index{equivalent under 
$\theta$-subsumption}, 
denoted $C\sim D$\index{$\sim$ (equivalent under $\theta$-subsump- \\tion)}, 
if and only if $C\preceq D$ and $D\preceq C$.
\end{definition}

$\theta$-subsumption is reflexive and transitive.
Two clauses may be equivalent under $\theta$-subsumption without being 
variants. Two clauses $C$ and $D$ are {\em variants}, denoted 
$C\simeq D$, if they are equal up to variable renaming. 

\begin{example}
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(x)\leftarrow q(x,y),\:q(y,z),\:q(z,w),\:q(w,x)\:),\\
D=(\:p(x)\leftarrow q(x,y),\:q(y,x),\:q(x,x)\:),$ and $\\
E=(\:p(x)\leftarrow q(x,x)\:).
\end{array}\]
We have $C\preceq D$ since $C\{z/x,w/y\}\subseteq D$, 
$D\preceq E$ since $D\{y/x\}\subseteq E$, 
and thus $C\preceq E$. 
We also have $E\preceq D$. 
Hence, $D\sim E$ and still $D\not\simeq E$.
\end{example}

Theorem \ref{TDotsbc} states that $\theta$-subsumption between clauses 
is decidable. This was first shown by Robinson \nocite{Rob65}(1965, page 39).

\begin{sloppypar}
\begin{theorem}
\label{TDotsbc}
\index{decidability of $\theta$-subsumption \\between clauses}
\index{theorem-ba@theorem \ref{TDotsbc}}
{\bf (Decidability of $\theta$-subsumption between clauses)} 
Let $C$ and $D$ be clauses. Then there exists a procedure to decide if 
$C \preceq D$.
\end{theorem}
\end{sloppypar}

As mentioned in the introduction, we are particularly interested 
in least general generalizations. The main reason is that a least general 
generalization includes the information of all consistent generalizations. 

\begin{definition}
A clause $C$ is a {\em generalization under $\theta$-sub\-sump\-tion}
\index{generalization under $\theta$-subsump\-tion} of a set of clauses
$S=\{D_{1},\ldots ,D_{n}\}$ if and only if, for every $1\leq i\leq n$, 
$C\preceq D_{i}$.
A generalization under $\theta$-subsumption $C$ of $S$ is a 
{\em least general generalization under $\theta$-sub\-sump\-tion}
\index{least general generalization under $\theta$-subsumption} 
(LGG$\theta$)\index{LGG$\theta$} of $S$ 
if and only if, for every generalization under 
$\theta$-subsumption $C'$ of $S$, $C'\preceq C$.
\end{definition}

\begin{example}
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(a)\leftarrow q(a),\:q(b)\:),\\
D=(\:p(b)\leftarrow q(b),\:q(x)\:),\\
E=(\:p(y)\leftarrow q(y),\:q(b)\:),$ and $\\
F=(\:p(y)\leftarrow q(y),\:q(b),\:q(z),\:q(w)\:).
\end{array}\]
Both clauses $E$ and $F$ are LGG$\theta$s of $\{C,D\}$.
\end{example}

In general, an LGG$\theta$ is not unique, as shown by the example above. 
However, it is unique up to $\theta$-subsumption equivalence. 
Plotkin has shown \nocite{Plo71b}(1971a, page 82) that there exists 
an LGG$\theta$ of every finite set of clauses. 

\begin{theorem}
\label{TEoLGGts}
\index{existence of LGG$\theta$s}
\index{theorem-bb@theorem \ref{TEoLGGts}}
{\bf (Existence of LGG$\theta$s)} 
Let $S$ be a finite set of clauses. Then there exists an LGG$\theta$ of $S$.
\end{theorem}

An LGG$\theta$ of a set of clauses is computable, and 
Plotkin has described \nocite{Plo71b}(1971a) an algorithm for that. 
This algorithm is quite simple and easy to implement, but computationally 
expensive. 



\subsection{Generalization under Implication}
\label{GuI}

Implication is the most natural and straightforward basis for generalization 
in inductive learning, since the concept of induction can be defined 
as the inverse of logically entailment. 

\begin{definition} 
A clause $C$ {\em implies}\index{implies} a clause $D$, 
denoted $C\Rightarrow D$\index{$\Rightarrow$ (implies)}, 
if and only if every 
model for $C$ is a model for $D$ ($\{C\}\models D$). 
% We say that $C$ is an {\em implicant} of $D$.
Two clauses $C$ and $D$ are {\em equivalent under 
implication}\index{equivalent under implication}, denoted 
$C\Leftrightarrow D$\index{$\Leftrightarrow$ (equivalent under implica\-tion)}, 
if and only if $C\Rightarrow D$ and $D\Rightarrow C$.\end{definition}

It is well-known that implication is reflexive and transitive. 
Two clauses may be equivalent under implication without 
being equivalent under $\theta$-subsumption.

\begin{example}
\label{exC}
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(x,y,z)\leftarrow p(y,z,x)\:),$ and $\\
D=(\:p(x,y,z)\leftarrow p(z,x,y)\:).
\end{array}\]
Then we have $C\Leftrightarrow D$, since $D$ is a resolvent 
of $C$ resolved with itself, and $C$ is a resolvent of $D$ 
resolved with itself. We also have $C\not\simeq D$, and even 
$C\not\sim D$.
\end{example}

It has been claimed that implication and $\theta$-subsumption are equivalent 
for function-free clauses \nocite{Hel87}(Helft, 1987). This is wrong as shown 
by the example above. 
The above example also shows that if a clause $C$ implies a clause $D$ 
then $C$ does not necessarily $\theta$-subsume $D$. 
It is well-known that implication is a strictly weaker relation between 
clauses than $\theta$-subsumption.

\begin{proposition}
\label{PimplB}
\index{proposition-cb@proposition \ref{PimplB}}
Let $C$ and $D$ be two clauses. If $C\preceq D$ then $C\Rightarrow D$.
\end{proposition}

Proposition \ref{PimplB} has been proved by Idestam-Almquist 
\nocite{Ide93e}(1993a, page 21). 
Unfortunately implication between clauses is problematic since it is 
undecidable, which has been proved by Schmidt-Schauss 
\nocite{Sch88}(1988, page 294).

\begin{theorem}
\label{TUoibc}
\index{undecidability of implication between clauses}
\index{theorem-ca@theorem \ref{TUoibc}}
{\bf (Undecidability of implication between clauses)} 
Let $C$ and $D$ be clauses. 
Then there exists no procedure to 
decide if $C\Rightarrow D$. 
\end{theorem}

Niblett \nocite{Nib88}(1988) has claimed that implication between Horn clauses 
is decidable. This result has later been proved to be false \cite{MP92}.

The definition of a least general generalization under implication (LGGI) 
follows the definition of an LGG$\theta$. 

\begin{definition}
A clause $C$ is a {\em generalization under implication}
\index{generalization under implication} of a set of clauses
$S=\{D_{1},\ldots ,D_{n}\}$ if and only if, for every $1\leq i\leq n$, 
$C\Rightarrow D_{i}$. 
A generalization under implication $C$ of $S$ is a 
{\em least general generalization under implication}
\index{least general generalization under implication} 
(LGGI)\index{LGGI} of $S$ 
if and only if, for every generalization under implication $C'$ of $S$, 
$C'\Rightarrow C$.
\end{definition}

\begin{example}
\label{exA}
Consider the following clauses:
\[ \begin{array}{l}
C=(\:p(f(a))\leftarrow p(a)\:),\\
D=(\:p(f^{2}(b))\leftarrow p(b)\:),\\
E=(\:p(f(x))\leftarrow p(y)\:),$ and $\\
F=(\:p(f(z))\leftarrow p(z)\:).
\end{array}\]
The clause $E$ is an LGG$\theta$ of $\{C,D\}$, and $F$ is an LGGI of $\{C,D\}$. 
The LGG$\theta$ (clause $E$) is strictly more general than the LGGI (clause $F$), 
both under implication and under $\theta$-subsumption, since $E\Rightarrow F$ but 
$F\not\Rightarrow E$, and $E\preceq F$ but $F\not\preceq E$. 
\end{example}

Whether there exists an LGGI of every finite set of clauses 
is still an open problem. 
However, since implication between clauses is undecidable, 
it is clear that in general an LGGI is not computable.



\subsection{T-implication}

Because implication between clauses is undecidable, we here introduce a 
stronger form of implication called T-implication, which is decidable 
between clauses. It is called T-implication since it is defined w.r.t.\ 
a finite set of ground terms $T$. 
In our presentation we use the notions of instance set of 
clauses, Skolem substitution, and term set of sets of clauses.

\begin{definition}
Let $C$ be a clause, $\{x_{1},\ldots,x_{n}\}$ the set of variables in $C$, 
and $T$ a set of terms. 
Then the {\em instance set}\index{instance set} 
${\cal I}(C,T)$\index{${\cal I}$ (instance set)} of $C$ w.r.t.\ $T$ is 
$\{C\theta\;|\;\theta=\{x_{1}/t_{1},\ldots,x_{n}/t_{n}\}\mbox{ where } 
\{t_{1},\ldots,\linebreak
t_{n}\}\subseteq T \}$.
\end{definition}

\begin{definition} 
Let $\sigma$ be a substitution, $C$ a clause, $\{x_{1},\ldots,x_{n}\}$ 
the set of variables occurring in $C$, $S$ a set of clauses, 
and $F$ the set of function symbols occurring in $S\cup\{C\}$.
Then $\sigma$ is a {\em Skolem substitution}\index{Skolem substitution} 
for $C$ w.r.t.\ $S$ if and only if 
$\{x_{1}/a_{1},\ldots,x_{n}/a_{n}\}\subseteq\sigma$ where 
$a_{1},\ldots,a_{n}$ are distinct constants, 
and $F\cap \{a_{1},\ldots,a_{n}\}=\emptyset$.  
\end{definition}

\begin{definition}
Let $\{D_{1},\ldots,D_{n}\}$ be a set of clauses such that 
$D_{1},\ldots,D_{n}$ have no variables in common, 
$S$ be a set of clauses, $\sigma$ a 
substitution, and $T$ a set of terms. 
Then $T$ is a {\em term set}\index{term set} 
of $\{D_{1},\ldots,D_{n}\}$ by $\sigma$ w.r.t.\ $S$ if and only if:\\
a) $\sigma$ is a Skolem substitution for 
$\{D_{1},\ldots,D_{n}\}$ w.r.t.\ $S$, and \\
b) $T$ is finite and includes all terms and subterms occurring in 
$\{D_{1},\ldots,D_{n}\}\sigma$.\\
If $T$ is equal to the set of terms and subterms occurring in 
$\{D_{1},\ldots,D_{n}\}\sigma$ then $T$ is a 
{\em minimal term set}\index{minimal term set} 
of $\{D_{1},\ldots,D_{n}\}$ by $\sigma$ w.r.t.\ $S$.
\end{definition}

\begin{definition}
Let $C$ and $D$ be clauses, and $T$ a term set of $\{D\}$ by $\sigma$ 
w.r.t.\ $\{C\}$. Then $C$ {\em T-implies} $D$\index{T-implies} w.r.t.\ $T$, 
denoted $C\Rightarrow_{T} D$\index{$\Rightarrow_{T}$ (T-implies)}, 
if and only if 
${\cal I}(C,T)\models D\sigma$. 
% We say that $C$ is a {\em T-implicant} of $D$ w.r.t.\ $T$.
Two clauses $C$ and $D$ are {\em equivalent under T-implication}\index{equivalent 
under T-implication} w.r.t.\ $T'$, denoted 
$C \Leftrightarrow_{T'} D$\index{$\Leftrightarrow_{T}$ 
(equivalent under T-impli\-cation)}, if and only if 
$C\Rightarrow_{T'}D$ and $D\Rightarrow_{T'}C$, where 
$T'$ is a term set of $\{C,D\}$. 
\end{definition}

Note that the definition of T-implication is independent of the choice of 
the Skolem substitution $\sigma$. 
In the following, if we say that a clause $C$ T-implies a clause $D$ without 
explicitly stating $T$, we mean that $C$ T-implies $D$ w.r.t.\ a minimal term 
set of $\{D\}$. Note that if $C$ T-implies $D$ w.r.t.\ a minimal term set of 
$D$ then $C$ T-implies $D$ w.r.t.\ any term set of $D$.

\begin{example}
\label{exD}
Consider the following clauses $C$ and $D$, substitution $\sigma$, set of 
terms $T$ and set of clauses ${\cal I}(C,T)$:
\[\begin{array}{l}
C=(\:p(f(x))\leftarrow p(x)\:),\\
D=(\:p(f^{2}(y))\leftarrow p(y)\:),\\
\sigma=\{y/a\},\\
T=\{a,f(a),f^{2}(a)\},$ and $\\
{\cal I}(C,T)=\{\:
(\:p(f(a))\leftarrow p(a)\:),\:\\
\hspace{54pt} (\:p(f^{2}(a))\leftarrow p(f(a))\:),\:\\
\hspace{54pt} (\:p(f^{3}(a))\leftarrow p(f^{2}(a))\:)\:\}.
\end{array}\]
Then $T$ is a minimal term set of $\{D\}$ by $\sigma$ w.r.t.\ $\{C\}$, 
and ${\cal I}(C,T)$ is the instance set of $C$ w.r.t.\ $T$. 
We have that ${\cal I}(C,T)\models D\sigma$ and thus 
$C\Rightarrow_{T} D$. 
Note that $C\Rightarrow D$, and that $C\not\preceq D$.
\end{example}

Like implication, T-implication is reflexive, but unlike implication, 
T-implication is not transitive \nocite{Ide93e}(Idestam-Almquist, 1993a). 
The relationship between implication and T-implication, described in 
Corollary \ref{CRbiaTi} below, follows from Herbrand's theorem. 
For a proof of Herbrand's theorem the reader is referred to a 
book by Chang and Lee \nocite{CL73}(1973, page 61). 
In our proof of Corollary \ref{CRbiaTi} we use the notion of the 
complement of a clause. 

\begin{definition}
Let $C=(A_{1},\ldots,A_{m}\leftarrow B_{1},\ldots ,B_{n})$ be a clause, 
$T$ a set of clauses, and $\sigma =\{x_{1}/a_{1},\ldots ,x_{k}/a_{k}\}$ a 
Skolem substitution for $C$ w.r.t.\ $T$. 
Then the set of ground unit clauses
$\{(\leftarrow A_{1})\sigma,\ldots,(\leftarrow A_{m})\sigma,
(B_{1}\leftarrow)\sigma,\ldots,(B_{n}\leftarrow)\sigma\}$ 
is the {\em complement}\index{complement} $\overline{C}$ 
of $C$ by $\sigma$ w.r.t.\ $T$. 
\end{definition}

\begin{theorem}
\label{THt}
\index{Herbrand's theorem}
\index{theorem-cb@theorem \ref{THt}}
{\bf (Herbrand's theorem)}
A set of clauses $S$ is unsatisfiable if and only if there exists a 
finite unsatisfiable set $S'$ of ground instances of clauses in $S$.
\end{theorem}

\begin{corollary}
\label{CRbiaTi}
\index{relationship between implication and T-implication}
\index{corollary-ca@corollary \ref{CRbiaTi}}
{\bf (Relationship between implication and T-impli\-cation)} 
Let $C$ and $D$ be clauses. Then:\\
a) if $C\Rightarrow_{T} D$ for some term set $T$ of $\{D\}$ then 
$C\Rightarrow D$, and \\
b) if $C\Rightarrow D$ then there exists a term set $T$ of $\{D\}$ 
such that $C\Rightarrow_{T}D$.
\end{corollary}

\begin{proof}
a) If $C\Rightarrow_{T} D$ then ${\cal I}(C,T)\models D\sigma$, where 
$T$ is a term set of $\{D\}$ by $\sigma$ w.r.t.\ $\{C\}$. 
Hence, ${\cal I}(C,T)\cup\overline{D}\models\bot$, where $\overline{D}$ 
is the complement of $D$ by $\sigma$. 
By Theorem \ref{THt}, $\{C\}\cup\overline{D}\models\bot$, and thus 
$C\Rightarrow D$.

b) If $C\Rightarrow D$ then $\{C\}\cup\overline{D}\models\bot$, where 
$\overline{D}$ is the complement of $D$ by $\sigma$ w.r.t.\ $\{C\}$. 
Then by Theorem \ref{THt}, there exists a term set $T$ of $\{D\}$ 
such that ${\cal I}(C,T)\cup\overline{D}\models\bot$, and thus 
${\cal I}(C,T)\models D\sigma$. 
Then by definition $C\Rightarrow_{T} D$.
\end{proof}

It follows from Corollary \ref{CRbiaTi} that T-implication can 
become an arbitrary good approximation of implication by extending 
the considered term set. 
T-implication is a strictly stronger relation between clauses than 
implication. The following example illustrates that if a clause $C$ 
implies a clause $D$ then $C$ does not necessarily T-imply $D$. 

\begin{example}
Consider the following clauses $C$, $D$ and $E$, and set of terms $T$:
\[\begin{array}{l}
C=(\:p(f(x),y)\leftarrow p(z,x)\:),\\
D=(\:p(f(x),y)\leftarrow p(z,w)\:),\\
E=(\:p(f(a),a)\leftarrow p(a,f(a))\:),$ and $\\
T=\{a,f(a)\}.
\end{array}\]
Then $C\Rightarrow E$ since $D$ is a resolvent of $C$ resolved with itself 
and $E$ is an instance of $D$. The set of terms $T$ is a minimal term set 
of $E$. We do not show here the whole set ${\cal I}(C,T)$, 
but just point out that ${\cal I}(C,T)\not\models E$ and thus 
$C\not\Rightarrow_{T} E$. However if we extend $T$ to $T'=\{a,f(a),f^{2}(a)\}$ 
then ${\cal I}(C,T')\models E$, and thus $C\Rightarrow_{T'}E$.
\end{example}

Below we show that if a clause $C$ $\theta$-subsumes a clause $D$ then $C$ 
also T-implies $D$. Thus, T-implication is a strictly weaker relation between 
clauses than $\theta$-subsumption. 
We also show decidability of T-implication between clauses. 

\begin{proposition}
\label{PimplE}
\index{proposition-cd@proposition \ref{PimplE}}
Let $C$ and $D$ be clauses and $T$ a term set of $\{D\}$. 
If $C\preceq D$ then $C\Rightarrow_{T} D$.
\end{proposition}

\begin{proof}
If $C\preceq D$ then there exists a substitution 
$\theta$ such that $C\theta\subseteq D$. 
Let $T$ be a term set of $\{D\}$ by $\sigma$ w.r.t.\ $\{C\}$. 
Then we have $C\theta\sigma\in {\cal I}(C,T)$. 
We also have $C\theta\sigma\subseteq D\sigma$, and thus 
$C\theta\sigma\preceq D\sigma$. 
Then by Proposition \ref{PimplB}, $C\theta\sigma\Rightarrow D\sigma$ 
$(\{C\theta\sigma\}\models D\sigma)$. 
Consequently ${\cal I}(C,T)\models D\sigma$, and then by definition 
$C\Rightarrow_{T} D$.
\end{proof}

\begin{theorem}
\label{TDoTibc}
\index{decidability of T-implication \\between clauses}
\index{theorem-cc@theorem \ref{TDoTibc}}
{\bf (Decidability of T-implication between clauses)} 
Let $C$ and $D$ be clauses and $T$ a term set of $\{D\}$. Then there exists 
a procedure to decide if $C\Rightarrow_{T} D$.
\end{theorem}

\begin{proof}
By the definition of T-implication we have ${\cal I}(C,T)\models D\sigma$ 
where $T$ is a term set of $D$ by $\sigma$ w.r.t.\ $\{C\}$. 
We have that ${\cal I}(C,T)$ is a set of ground clauses and $D\sigma$ is a 
ground clause. 
Thus, it follows from the decidability of logical consequence in 
propositional logic that T-implication is decidable.
\end{proof}



\subsection{Generalization under T-implication}

A least general generalization under T-implication (LGGT) is defined 
similar to an LGG$\theta$ and an LGGI. 

\begin{definition}
Let $C$ be a clause, $S=\{D_{1},\ldots,D_{n}\}$ a set of clauses, and 
$T$ a term set of $S$ w.r.t.\ $\{C\}$. 
Then $C$ is a {\em generalization under T-implication}
\index{generalization under T-implica- \\tion} of $S$ w.r.t.\ $T$ 
if and only if, for every $1\leq i\leq n$, $C\Rightarrow_{T} D_{i}$. 
A generalization under T-implication $C$ of $S$ w.r.t.\ $T$ is a 
{\em least general generalization under T-implication}
\index{least general generalization under T-implication} 
(LGGT)\index{LGGT} of $S$ w.r.t.\ $T$ 
% if and only if $C'\Rightarrow_{T}C$ for every generalization 
% under T-implication $C'$ of $S$ w.r.t.\ $T$.
if and only if, for every generalization under T-implication $C'$ of 
$S$ w.r.t.\ $T$, $C'\Rightarrow_{T'}C$, where $T'$ is a minimal term 
set of $C$. 
\end{definition}

\begin{example}
Consider the following clauses:
\[ \begin{array}{l}
C=(\:p(f(a))\leftarrow p(a)\:),\\
D=(\:p(f^{2}(b))\leftarrow p(b)\:),\\
E=(\:p(f(x))\leftarrow p(y)\:),$ and $\\
F=(\:p(f(z))\leftarrow p(z)\:).
\end{array}\]
The clause $E$ is an LGG$\theta$ of $\{C,D\}$, and $F$ is both an 
LGGI and an LGGT of $\{C,D\}$. 
The LGGT is strictly more specific than the LGG$\theta$, since 
$E\Rightarrow F$ and $F\not\Rightarrow E$. 
\end{example}

% In \cite[page 29]{Ide93e} it is proved that there exists an LGGT of 
% every finite set of clauses. 
% 
% \begin{theorem}
% \label{TEoLGGTs}
% \index{existence of LGGTs}
% \index{theorem-ce@theorem \ref{TEoLGGTs}}
% {\bf (Existence of LGGTs)} 
% Let $S$ be a finite set of clau\-ses, and $T$ a term set of $S$. 
% Then there exists an LGGT of $S$ w.r.t.\ $T$.
% \end{theorem}


Below we prove that there exists an LGGT of every finite set of 
clauses. In fact we prove something stronger, namely that there exists, 
what we call, a complete LGGT of every finite set of non-tautological clauses. 
Note that a complete LGGT is $\theta$-subsumed by any other generalization 
under T-implication. 

\begin{definition}
Let $C$ be an LGGT of a set of clauses $S$ w.r.t.\ a term set $T$. 
Then $C$ is a {\em complete LGGT} of $S$ w.r.t.\ $T$ if and only if, 
for every generalization under T-implication $C'$ of $S$ w.r.t.\ $T$, 
$C'\preceq C$.
\end{definition}

If $C$ is a clause then we let $C^{+}$ denote the set of positive literals 
in $C$, and $C^{-}$ the set of negative literals in $C$. 
The following proposition has been proved by Gottlob \nocite{Got87}(1987, page 110). 


\begin{proposition}
\label{PimplC}
\index{proposition-ce@proposition \ref{PimplC}}
Let $C=C^{+}\cup C^{-}$ be a clause and $D=D^{+}\cup D^{-}$ a 
non-tautological clause. 
If $C\Rightarrow D$ then $C^{+}\preceq D^{+}$ and $C^{-}\preceq D^{-}$.
\end{proposition}

\begin{lemma}
\label{LimplB}
\index{lemma-ca@lemma \ref{LimplB}}
Let $S$ be a finite set of non-tautological clauses, 
$T=\{t_{1},\ldots,t_{m}\}$ a term set of $S$, 
$V=\{x_{1},\ldots,x_{m}\}$ a set of variables, 
and $G=\{C_{1},C_{2},\ldots\}$ the (possibly infinite) set of all 
generalizations under T-implication of $S$ w.r.t.\ $T$. 
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 a clause in $S$, and 
$F_S$ and $F_G$ the sets of predicate and function symbols occurring 
in the clauses in $S$ and $G$ respectively. 
Then $F_G \cup V$ is the set of variables, predicate and function symbols 
occurring in the clauses in $G'$. 
By Corollary \ref{CRbiaTi}, $G$ is a set of generalizations under 
implication of $S$. 
Then, by Proposition \ref{PimplC} and the definition of $\theta$-subsumption, 
$F_G \subseteq F_S$ and the maximal depth of a clause in $G$ is $d$. 
Hence $F_G \cup V$ is finite and the maximal depth of a clause in $G'$ 
is $d$, and consequently $G'$ is a finite set of clauses. 
\end{proof}

\begin{lemma}
\label{LimplA}
\index{lemma-cb@lemma \ref{LimplA}}
Let $C$ be a clause, $S$ a set of clauses, $V=\{x_{1},\ldots,x_{m}\}$ a set 
of variables, and $T=\{t_{1},\ldots,t_{m}\}$ a term set of $S$ by $\sigma$ 
w.r.t\ $\{C\}$, such that $C$ is a generalization under T-implication of $S$ 
w.r.t.\ $T$. 
Then there exists an LGG$\theta$ $E$ of ${\cal I}(C,V)$ such that 
$E$ is a generalization under T-implication of $S$ w.r.t.\ $T$. 
\end{lemma}

\begin{proof}
Let ${\cal I}(C,V)=\{C\rho_{1},\ldots,C\rho_{k}\}$. 
Then, $\rho_{1},\ldots,\rho_{k}$ are variable-pure substitutions, and 
for every LGG$\theta$ $F$ of ${\cal I}(C,T)$ and every $1\leq i\leq k$, 
we have $C\preceq F$ and $F\preceq C\rho_i$. 
Then, there exists an LGG$\theta$ $E$ of ${\cal I}(C,T)$ and variable-pure 
substitutions $\theta_1,\ldots,\theta_k$ such that, for every $1\leq i\leq k$, 
$E\theta_i\subseteq C\rho_i$. 

Let $\gamma=\{x_{1}/t_{1},\ldots,x_{m}/t_{m}\}$, and 
then ${\cal I}(C,T)=\{C\rho_{1}\gamma,\ldots,C\rho_{k}\gamma\}$. 
Since $C$ is a generalization under T-implication of $S$ w.r.t.\ $T$, 
we have $\{C\rho_1\gamma,\ldots,C\rho_k\gamma\}\models S\sigma$. 
For every $1\leq i\leq k$, $E\theta_{i}\gamma\preceq C\rho_{i}\gamma$. 
Then, for every $1\leq i\leq k$, by Proposition \ref{PimplB}, 
$E\theta_{i}\gamma\Rightarrow C\rho_{i}\gamma$, and thus 
$\{E\theta_{1}\gamma,\ldots,E\theta_{k}\gamma\}\models 
\{C\rho_{1}\gamma,\ldots,C\rho_{k}\gamma\}$. 
Since $\theta_{1},\ldots,\theta_{k}$ are variable-pure substitutions, 
we have $\{E\theta_{1}\gamma,\ldots,E\theta_{k}\gamma\}\subseteq {\cal I}(E,T)$. 
Thus, ${\cal I}(E,T)\models \{C\rho_{1}\gamma,\ldots,C\rho_{k}\gamma\}$, and 
${\cal I}(E,T)\models S\sigma$. 
Consequently $E$ is a generalization under T-implication of $S$ w.r.t.\ $T$. 
\end{proof}

\begin{lemma}
\label{LimplC}
\index{lemma-cc@lemma \ref{LimplC}}
Let $C$, $D$ and $E$ be clauses such that $C$ and $D$ have no variables in 
common, and let $T$ be a term set of $\{E\}$ by $\sigma$ w.r.t.\ $\{C,D\}$. 
If $C\Rightarrow_{T} E$ and $D\Rightarrow_{T} E$ then 
$C\cup D\Rightarrow_{T} E$.
\end{lemma}

\begin{proof}
If $C\Rightarrow_{T} E$ and $D\Rightarrow_{T} E$ then by definition 
${\cal I}(C,T)\models E\sigma$ and ${\cal I}(D,T)\models E\sigma$. 
Let ${\cal I}(C,T)=\{C_{1},\ldots,C_{n}\}$ and 
${\cal I}(D,T)=\{D_{1},\ldots,D_{m}\}$. Then 
${\cal I}(C\cup D,T)=\{C_{i}\cup D_{j}\;|\; 1\leq i\leq n$ and $1\leq j\leq m\}$. 
Let $I$ be a model for ${\cal I}(C\cup D,T)$. 
Then, for every $1\leq i\leq n$ and $1\leq j\leq m$, $I$ is a model for 
$C_{i}\cup D_{j}$. 
Hence if $I$ is not a model for $C_{i}$ for some $1\leq i\leq n$ then 
$I$ must be a model for $D_{j}$ for every $1\leq j\leq m$. 
Then it follows that either $I$ is a model for ${\cal I}(C,T)$ or 
$I$ is a model for ${\cal I}(D,T)$, and thus $I$ is a model for $E\sigma$. 
Consequently, ${\cal I}(C\cup D,T)\models E\sigma$, and then by definition 
$C\cup D\Rightarrow_{T} E$.
\end{proof}

\begin{theorem}
\label{TEosLGGTs}
\index{existence of complete LGGTs}
\index{theorem-cd@theorem \ref{TEosLGGTs}}
{\bf (Existence of complete LGGTs)} 
Let $S$ be a finite set of non-tautological clauses, and $T$ a term set 
of $S$. Then there exists a complete LGGT of $S$ w.r.t.\ $T$.
\end{theorem}

\begin{proof}
Let $T=\{t_{1},\ldots,t_{m}\}$, $V=\{x_{1},\ldots,x_{m}\}$ be a set of 
variables, and $G=\{C_{1},C_{2},\ldots\}$ the (possibly infinite) set of 
all generalizations under T-implication of $S$ w.r.t.\ $T$. 
By Lemma \ref{LimplB}, 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 
$\{{\cal I}(C_{1},V),{\cal I}(C_{2},V),\ldots\}$ is also finite.
 
For every $i\geq 1$, by Lemma \ref{LimplA}, there exists an LGG$\theta$ 
$E_i$ of ${\cal I}(C_i,V)$ such that $E_i$ is a generalization under 
T-implication of $S$ w.r.t.\ $T$. 
Then rename the variables in $E_1,E_2,\ldots$ such that, for every $k\geq 1$ 
and $p\geq 1$, $E_k=E_p$ whenever ${\cal I}(C_k,V)={\cal I}(C_p,V)$ and 
otherwise $E_k$ and $E_p$ have no variables in common. 
Then the set $\{E_{1},E_{2},\ldots\}$ is finite, since 
$\{{\cal I}(C_{1},V),{\cal I}(C_{2},V),\ldots\}$ is finite. 
Let $F=E_{1}\cup E_{2}\cup\ldots$, which consequently is a clause.

For every $i\geq 1$, by the definition of an LGG$\theta$, $C_{i}\preceq E_{i}$, 
and thus $C_{i}\preceq F$. 
Then, for every $i\geq 1$, by Proposition \ref{PimplE}, $C_i\Rightarrow_T F$. 
As showed above, for every $i\geq 1$, $E_i$ is a generalization under T-implication of 
$S$ w.r.t.\ $T$. Then, by Lemma \ref{LimplC}, $F$ is a generalization under 
T-implication of $S$ w.r.t.\ $T$. 
Consequently, $F$ is a complete LGGT of $S$ w.r.t.\ $T$. 
\end{proof}

\begin{theorem}
\label{TEoLGGTs}
\index{existence of LGGTs}
\index{theorem-ce@theorem \ref{TEoLGGTs}}
{\bf (Existence of LGGTs)} 
Let $S$ be a finite set of clau\-ses, and $T$ a term set of $S$. 
Then there exists an LGGT of $S$ w.r.t.\ $T$.
\end{theorem}

\begin{proof}
Let $D$ be a tautology and $\sigma$ a Skolem substitution for $D$. Then 
$\top\models D\sigma$, and thus for every clause $C$, $C\Rightarrow_{T} D$. 
If every clause in $S$ is a tautology, then every clause is a generalization 
under T-implication of $S$ w.r.t.\ $T$, and every tautology is an LGGT of 
$S$ w.r.t.\ $T$. 
Let $S'$ be the set of clauses obtained from $S$ by removing all tautologies. 
It is clear that every generalization under T-implication of $S$ w.r.t.\ $T$ 
also is a generalization under T-implication of $S'$ w.r.t.\ $T$. 
By Theorem \ref{TEosLGGTs}, there exists an LGGT of $S'$ w.r.t.\ $T$. 
Consequently there exists an LGGT of $S$.
\end{proof}




\section{Reduction of Implication to $\theta$-subsumption}
\label{RoItts}

There are generalizations under 
implication that are not generalizations under $\theta$-subsump\-tion. 
Our main idea to find all generalizations under implication, is to reduce 
implication to $\theta$-subsumption, which can be achieved by inverting 
self-resolution. In this section we will describe a technique for inverting 
resolution based on or-introduc\-tion of literals. We will also introduce 
the notion of expansion of clauses, which summarizes our idea of reduction 
of implication to $\theta$-subsumption.



\subsection[Difference between $\theta$-subsumption and Implication]{Difference 
between $\theta$-subsumption and Implication}
\label{sDbtsaI}

In section \ref{GuI}, we showed that $C\Rightarrow D$ 
follows from $C\preceq D$, but not the converse. Hence, there are 
generalizations under implication that are not generalizations under 
$\theta$-subsumption. 
It follows from a result by Gottlob \nocite{Got87}(1987) that the difference 
between $\theta$-subsump\-tion and implication only concerns ambivalent 
clauses, as defined below. 

\begin{definition}
A clause $C$ is {\em ambivalent}\index{ambivalent} if and only if 
there exist a positive literal $A \in C$ and a negative literal 
$B \in C$ such that $A$ and $B$ have the same predicate symbol. 
\end{definition}

\begin{example}
The clause
\[ C=(\:p(f^{2}(a))\leftarrow q(b),\:p(a)\:) \]
is ambivalent since $p(f^{2}(a))$ and $\neg p(a)$ have the same 
predicate symbol. 
However, $C$ is not recursive since neither $p(a)$ nor $q(b)$ 
is unifiable with a variant of $p(f^{2}(a))$.
\end{example}

\begin{proposition}
\label{PredD}
\index{proposition-da@proposition \ref{PredD}}
Let $C$ be a clause and $D$ a non-ambivalent clause. 
Then $C\Rightarrow D$ if and only if $C\preceq D$.
\end{proposition}

Proposition \ref{PredD} has been proved by Gottlob 
\nocite{Got87}(1987, page 110). 
It follows from this proposition that an LGG$\theta$ and an LGGI of a set 
of clauses, including at least one non-ambivalent clause, are equivalent. 

Muggleton \nocite{Mug92}(1992) has investigated the relationship between 
resolution and implication between clauses. He describes the subsumption 
theorem \cite{Lee67} in terms of input resolution, and gives a corollary 
about the relationship between $\theta$-subsumption and implication between 
clauses. 
Unfortunately, this formulation of the subsumption theorem, which later also has 
been used by Idestam-Almquist \nocite{Ide93,Ide93e}(1993c, 1993a), has been shown 
to be wrong. 
Nienhuys-Cheng and de Wolf \nocite{NW95}(1995) have given a counter-example 
which shows that the subsumption theorem for input resolution does not even 
hold in the special case where the considered set of clauses contains only 
one clause. 
Below we give the correct formulation of the subsumption theorem, 
which is based on the $n$th resolution \cite{Rob65}. 

\begin{definition} 
A substitution $\theta$ is a {\em unifier} for a finite set of literals 
$S$ if and only if $S\theta$ is a singleton. A unifier $\theta$ 
for $S$ is a {\em most general unifier} (mgu) for $S$ if and only if for each 
unifier $\sigma$ of $S$ there exists a substitution $\gamma$ such that 
$\sigma=\theta \gamma$.  
\end{definition}

\begin{definition}
Let $C$ be a clause, $\Gamma\subseteq C$ and $\gamma$ an mgu of $\Gamma$.
Then $C\gamma$ is a {\em factor}\index{factor} of $C$.
\end{definition}

\begin{definition} 
A clause $R$ is a {\em resolvent}\index{resolvent} 
of two clauses $C$ and $D$ if and 
only if there are $C\gamma$, $D\mu$, $A$, $B$ and $\theta$ such that:\\
a) $C\gamma$ is a factor of $C$ and $D\mu$ is a factor of $D$, \\
b) $C\gamma$ and $D\mu$ have no variables in common, \\
c) $A$ is a literal in $C\gamma$ and $B$ is a literal in $D\mu$, \\
d) $\theta$ is an mgu of $\{A,\overline{B}\}$, and \\
e) $R$ is the clause $((C\gamma-\{A\})\cup (D\mu-\{B\}))\theta$. \\
The clauses $C$ and $D$ are called {\em parent clauses}\index{parent clauses} 
of $R$. 
\end{definition}

\begin{definition} 
Let $T$ be a set of clauses. Then, the 
{\em nth resolution}\index{nth resolution@$n$th resolution} of $T$, 
denoted ${\cal R}^{n}(T)$\index{${\cal R}^{n}$ ($n$th resolution)}, 
is defined as: \\
a) ${\cal R}^{0}(T)=T$, and \\
b) ${\cal R}^{n}(T)={\cal R}^{n-1}(T)\cup
\{R \; | \; C,D\in {\cal R}^{n-1}(T)$ and $R$ is a 
resolvent of $C$ and $D\}$ if $n>0$.
\end{definition}

\begin{theorem}
\label{TSt}
\index{subsumption theorem}
\index{theorem-da@theorem \ref{TSt}}
{\bf (Subsumption theorem)} 
Let $T$ be a set of clauses and $C$ a non-tautological
clause. Then $T \models C$ if and only if there exists a 
clause $D\in {\cal R}^{n}(T)$ such that $D\preceq C$ for some $n\geq 0$.
\end{theorem}

Two different recent proofs of Theorem \ref{TSt} have been presented, 
one by Nienhuys-Cheng and de Wolf \nocite{NW95}(1995), and one by 
Bain and Muggleton \nocite{BM92}(1992). There also exist at least two 
different earlier proofs of this theorem in the literature, one by 
Slagle, Chang and Lee \nocite{SCL69}(1969), and one by Kowalski 
\nocite{Kow70}(1970). 
We are interested in the number of resolutions involved in the 
computation of a clause, and therefore we introduce the notion 
of $n$th resolution layer. A clause in the $n$th resolution 
layer has been obtained from the original set of clauses by 
$n-1$ resolutions. 

\begin{definition} 
Let $T$ be a set of clauses. Then, the 
{\em nth resolution layer} of $T$, denoted ${\cal L}^{n}(T)$, 
is defined as: \\
a) ${\cal L}^{1}(T)=T$, and \\
b) ${\cal L}^{n}(T)=\{R \; | \; R$ is a resolvent of 
$C\in {\cal L}^{m}(T)$ and $D\in {\cal L}^{p}(T)$ where 
$m+p=n-1$, $m\geq 1$ and $p\geq 1 \}$ if $n>1$.
\end{definition}

\begin{sloppypar}
\begin{corollary}
\label{CIbcur}
\index{implication between clauses using resolution}
\index{corollary-da@corollary \ref{CIbcur}}
{\bf (Implication between clauses using resolution)} 
Let $C$ be a clause and $D$ a non-tautological clause. Then $C\Rightarrow D$ if 
and only if there exists a clause $E\in {\cal L}^{n}(\{C\})$ such that 
$E\preceq D$ for some $n\geq 1$.
\end{corollary}
\end{sloppypar}

Corollary \ref{CIbcur} follows from Theorem \ref{TSt}, and the 
observation that, for every $n\geq 1$, if a clause $C\in {\cal L}^{n}(T)$ 
then also $C\in {\cal R}^{n}(T)$.
This corollary tells us that implication between clauses is equivalent to 
a combination of self-resolution and $\theta$-subsumption.
Muggleton \nocite{Mug92}(1992) has introduced the notion of powers and roots 
of clauses for specializations and generalizations of clauses 
where the clauses are resolved with themselves. 
Below we present definitions of these and related concepts modified 
w.r.t.\ the correct definition of the subsumption theorem. 

\begin{definition} 
A clause $D$ is an {\em $n$th power}
\index{nth power@$n$th power}\index{power} 
of a clause $C$ if and only if $D$ is
a variant of a clause in ${\cal L}^{n}(\{C\})$ ($n\geq 1$). We also say that 
$C$ is an {\em $n$th root}
\index{nth root@$n$th root}\index{root} 
of $D$.  
A clause $D$ is an 
{\em indirect $n$th power}\index{indirect $n$th power} 
of a clause $C$ if
and only if there exists a clause $E$ such that $E \preceq D$ and $E$ is an
$n$th power of $C$. We also say that $C$ is an 
{\em indirect $n$th root}\index{indirect $n$th root} of $D$.

Let $C$ be a clause and $D$ an indirect $n$th power of $C$. Then $D$ is a 
{\em proper indirect $n$th power}\index{proper indirect $n$th power} of $C$ 
if and only if $C\not\preceq D$. 
We also say that $C$ is a 
{\em proper indirect $n$th root}\index{proper indirect $n$th root} of $D$.
\end{definition}

\begin{example} 
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(f(x))\leftarrow p(x)\:),\\
D=(\:p(f^{2}(x))\leftarrow p(x)\:),\\
E=(\:p(f^{3}(x))\leftarrow p(x)\:),\\
F=(\:p(f^{2}(a))\leftarrow p(a),\:p(b)\:),$ and $\\ 
G=(\:p(x)\leftarrow p(b)\:).
\end{array}\]
The clause $C$ is a second root of $D$, and a third root of $E$. 
The clause $C$ is also an indirect second root of $F$, since $C$ is a 
second root of $D$ and $D$ $\theta$-subsumes $F$. In fact $C$ is a proper 
indirect second root of $F$, since $C\not\preceq F$. 
For every $n\geq 1$, the clause $G$ is an indirect $n$th root of itself, 
but none of these indirect roots is a proper indirect root. 
\end{example}

To say that a clause implies another non-tautological clause or to say that 
the clause is an indirect root of the other clause, is equivalent. However, 
to say that a clause is an indirect $n$th root for some specified $n$ is more 
informative. 

Implication between clauses can be described as a 
combination of self-resolu\-tion and $\theta$-subsumption. 
Plotkin's algorithm to compute LGG$\theta$s 
gives us a suitable tool for finding generalizations under 
$\theta$-subsump\-tion. 
Hence, to be able to find generalizations under 
implication we also need a technique to invert resolution.



\subsection{Inverting One Resolution by Or-introduction}
\label{sIORbOi}

Other work on inverting resolution has 
primarily considered the problem of constructing one parent clause given 
the resolvent and the other parent clause 
\cite{MB88,RP89,Wir89,Mug90,HS91,Ide92,Rou92}. 
Below we will describe how or-introduction can be 
used to construct two parent clauses from only the resolvent. 
Let $C$ and $D$ be clauses, and the following clause $R$ a resolvent of 
$C$ and $D$:
\[ 
R=((C\gamma-\{A\})\cup(D\mu-\{B\}))\theta, 
\]
where $C\gamma$ is a factor of $C$, $D\mu$ is a factor of $D$, $A\in C\gamma$, 
$B\in D\mu$ and $\theta$ is an mgu for $\{A,\overline{B}\}$.
We seek parent clauses of $R$ that are minimally general. 
Then we should let $\gamma$, $\mu$ and $\theta$ be empty substitutions, 
which corresponds to an assumption that no instantiation of variables has 
been done in the resolution of $C$ and $D$, and thus we have 
$A=\overline{B}$. 
We should also let $C-\{A\}=D-\{B\}$, which corresponds to an assumption 
that each literal in $R$ is inherited both from $C$ and $D$. 
Then we have 
\[\begin{array}{l}
C=R\cup\{A\}$ and $D=R\cup\{\overline{A}\},
\end{array}\]
where $A$ could be any literal, and we say that $C$ and $D$ are obtained 
>from $R$ by or-introduction of the literal $A$. 

\begin{example}
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(f^{2}(a))\leftarrow p(f(a)),\:p(a)\:), \\
D=(\:p(f^{2}(a)),p(f(a))\leftarrow p(a)\:),$ and $\\
R=(\:p(f^{2}(a))\leftarrow p(a)\:).
\end{array}\]
The clauses $C$ and $D$ are parent clauses of $R$. 
\end{example}

The above technique to find parent clauses can be used to reduce implication 
to $\theta$-subsumption. This is of interest for ambivalent clauses, 
such as $R$ in the example above, for which there are proper indirect roots. 
For example the clause
\[ 
G=(\:p(f(x))\leftarrow p(x)\:) 
\]
is a proper indirect second root of $R$, and it 
$\theta$-subsumes both $C$ and $D$.

Proposition \ref{PredG} shows that the set of two clauses obtained by our 
technique for inverting one resolution is logically equivalent to the original 
clause. In Proposition \ref{PredF} it is shown that or-introduction of one 
literal is a general technique for inverting one resolution. 

\begin{proposition}
\label{PredG}
\index{proposition-db@proposition \ref{PredG}}
Let $R$ be a clause and $L$ a literal. 
Then $\{R\}\equiv\{ R \cup\{L\},R \cup \{ \overline{L}\} \}$.
\end{proposition}

\begin{proof}
Since $R\subseteq R\cup\{L\}$ and 
$R\subseteq R\cup\{\overline{L}\}$, we have 
$R\preceq R\cup\{L\}$ and $R\preceq R\cup\{\overline{L}\}$. 
Then by Proposition \ref{PimplB}, $R\Rightarrow R\cup\{L\}$ and 
$R\Rightarrow R\cup\{\overline{L}\}$. Thus 
$\{R\}\models \{R\cup\{L\},R\cup\{\overline{L}\}\}$.

The clause $R$ is a resolvent of $R\cup\{L\}$ and 
$R\cup\{\overline{L}\}$. Then by soundness of resolution, 
$\{R\cup\{L\},R\cup\{\overline{L}\}\} \models \{R\}$. 
Consequently, $\{R\}\equiv\{ R \cup\{L\},R \cup \{ \overline{L}\} \}$.
\end{proof} 

\begin{proposition}
\label{PredF}
\index{proposition-dc@proposition \ref{PredF}}
Let $C$ and $D$ be clauses and $R$ a resolvent of $C$ and $D$.
Then there exists a literal $L$ such that 
$C\preceq R\cup\{L\}$ and $D\preceq R\cup\{\overline{L}\}$.
\end{proposition}

\begin{proof}
By the definition of a resolvent we have 
$R=((C\gamma-\{A\})\cup(D\mu-\{B\}))\theta,$
where $C\gamma$ is a factor of $C$, 
$D\mu$ is a factor of $D$, $A\in C\gamma$, $B\in D\mu$ and 
$A\theta=\overline{B}\theta$ where $\theta$ is 
an mgu for $\{A,\overline{B}\}$.
Let $L=A\theta$, and then 
$R\cup\{L\}=(C\gamma\cup(D\mu-\{B\}))\theta$, and 
$R\cup\{\overline{L}\}=((C\gamma-\{A\})\cup D\mu)\theta$ since 
$A\theta=\overline{B}\theta$. 
Hence $C\gamma\theta\subseteq(C\gamma\cup(D\mu-\{B\}))\theta$
and $D\mu\theta\subseteq((C\gamma-\{A\})\cup D\mu)\theta$, and 
consequently $C\preceq R\cup\{L\}$ and $D\preceq R\cup\{\overline{L}\}$. 
\end{proof}



\subsection{Inverting Multiple Resolutions by Or-introduction}
\label{sIMRbOi}

The technique for inverting one resolution can be generalized to 
a technique for inverting a sequence of resolutions as follows. 
The set 
\[ 
\{R\cup\{L_1\},R\cup\{\overline{L_1}\}\}, 
\]
where $R$ is a clause and $L_1$ is a literal, is a set of two 
clauses from which the clause $R$ follows by one resolution. 
Similarly, the two sets 
\[\begin{array}{l}
\{R\cup\{L_1\}\cup\{L_2\},R\cup\{L_1\}\cup\{\overline{L_2}\},
R\cup\{\overline{L_1}\}\},$ and $\\
\{R\cup\{L_1\},R\cup\{\overline{L_1}\}\cup\{L_2\},R\cup
\{\overline{L_1}\}\cup\{\overline{L_2}\}\},
\end{array}\]
where $R$ is a clause and $L_1$ and $L_2$ are literals,
are sets of three clauses from which $R$ follows by two 
resolutions. In the same way, for given literals $L_1$, $L_2$ and 
$L_3$, we have six different sets of four clauses from which $R$ 
follows by three resolutions, and so on. 
All these sets are or-introduced from the clause $R$.

\begin{definition}
Let $C$ be a clause and $\Omega$ a sequence of literals. 
Then a set of clauses $S$ is {\em or-introduced}\index{or-introduced} 
>from $C$ by $\Omega$ if and only if either:\\
a) $S=\{C\}$ and $\Omega=[]$, or \\
b) $S=(S'-\{D\})\cup\{D\cup\{L\},D\cup\{\overline{L}\}\}$ and 
$\Omega=[L_{1},\ldots,L_{n},L]$, where $S'$ is a set of clauses or-introduced 
>from $C$ by $[L_{1},\ldots,L_{n}]$ and $D\in S'$.
\end{definition}

\begin{example}
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(f^{3}(a))\leftarrow p(a)\:), \\
D_{1}=(\:p(f^{3}(a)),\:p(f^{2}(a))\leftarrow p(a)\:), \\
D_{2}=(\:p(f^{3}(a))\leftarrow p(f^{2}(a)),\:p(a)\:), \\
E_{1}=(\:p(f^{3}(a)),\:p(f^{2}(a)),\:p(f(a)\leftarrow p(a)\:),$ and $\\
E_{2}=(\:p(f^{3}(a)),\:p(f^{2}(a))\leftarrow p(f(a)),\:p(a)\:).
\end{array}\]
The set of clauses $\{D_{1},D_{2}\}$ is or-introduced from $C$ by 
$[p(f^{2}(a))]$, and the set of clauses $\{E_{1},E_{2}\}$ is or-introduced from 
$D_{1}$ by $[p(f(a))]$. Consequently, the set of clauses 
$\{D_{2}, E_{1},E_{2}\}$ is or-introduced from $C$ by 
$[p(f^{2}(a)),\:p(f(a))]$.
\end{example}

In the example above, clause $D_{1}$ is a resolvent of $E_{1}$ and $E_{2}$, and 
$C$ is a resolvent of $D_{1}$ and $D_{2}$. Consequently, $C$ is derivable from 
$\{D_{2},E_{1},E_{2}\}$ by resolution. 
That a set of clauses or-introduced from a clause  is logically equivalent 
to the clause, is shown by the following theorem. 

\begin{sloppypar}
\begin{theorem}
\label{TEpooi}
\index{equivalence preservation of or-introduction}
\index{theorem-db@theorem \ref{TEpooi}}
{\bf (Equivalence preservation of or-introduction)} 
Let $S$ be a set of clauses or-introduced from a clause $C$ by a sequence 
of literals $[L_1,\ldots,L_n]$. 
Then $S\equiv \{C\}$.
\end{theorem}
\end{sloppypar}

\begin{proof}
The proof is by mathematical induction on $n$. It should be noted that $S$, 
in the statement of the theorem, in the proof is indexed by $n$. 

{\em Base step (n=0)}: $S_{0}$ is or-introduced from $C$ by $[]$. 
Hence $S_{0}\equiv\{C\}$.

{\em Induction hypothesis (n=k)}: $S_{k}\equiv\{C\}$, where $S_{k}$ is 
or-introduced from $C$ by $[L_{1},\ldots,L_{k}]$.

{\em Induction step (n=k+1)}: Let $D\in S_{k}$. Then 
$S_{k+1}=(S_{k}-\{D\})\cup\{D\cup\{L_{k+1}\},D\cup\{\overline{L_{k+1}}\}\}$ 
is or-introduced from $C$ by $[L_{1},\ldots,L_{k},L_{k+1}]$. 
By Proposition \ref{PredG}, we have 
$\{D\cup\{L_{k+1}\},D\cup\{\overline{L_{k+1}}\}\} \equiv \{D\}$, and 
consequently $S_{k+1}\equiv S_{k}$. By the induction hypothesis 
$S_{k}\equiv\{C\}$, and thus $S_{k+1}\equiv\{C\}$.
\end{proof}

In section \ref{sIORbOi} we showed that it is possible to invert one 
resolution by or-introduction of one literal. Below we show that it is 
possible to invert a sequence of resolutions by or-introduction of a 
sequence of literals.

\begin{lemma}
\label{LredE}
\index{lemma-da@lemma \ref{LredE}}
Let $D$ and $E$ be clauses, $\{C_1,\ldots,C_n\}$ a set of clauses, and 
$\{D_{1},\ldots,D_{n}\}$ a set of clauses or-introduced from $D$, such that 
$D\preceq E$ and, for every $1\leq i\leq n$, $C_i\preceq D_{i}$. 
Then there exists a set of clauses $\{E_{1},\ldots,E_{n}\}$ or-introduced 
>from $E$, such that for every $1\leq i\leq n$, $C_i\preceq E_{i}$.
\end{lemma}

\begin{proof}
Let $D_{i}$ be an arbitrary clause in $\{D_{1},\ldots,D_{n}\}$. Then we have 
$D_{i}=D\cup\Lambda_{i}$ for some set of literals $\Lambda_{i}$, since 
$\{D_{1},\ldots,D_{n}\}$ is or-introduced from $D$. 
Since $C_i\preceq D_i$, there exists a substitution $\theta_{i}$ such that 
$C_i\theta_{i}\subseteq D\cup\Lambda_{i}$. 
Since $D\preceq E$, there exists a substitution $\sigma$ such that 
$D\sigma\subseteq E$. Thus we have 
$(D\cup\Lambda_{i})\sigma\subseteq(E\cup\Lambda_{i}\sigma)$, and consequently 
$C_i\theta_{i}\sigma\subseteq E\cup\Lambda_{i}\sigma$. Let 
$E_{i}=E\cup\Lambda_{i}\sigma$ and we have $C_i\preceq E_{i}$.
\end{proof}

\begin{theorem}
\label{TIruoi}
\index{inverting resolution using or-in- \\troduction}
\index{theorem-dc@theorem \ref{TIruoi}}
{\bf (Inverting resolution using or-introduction)} 
Let $T$ be a set of clauses, $D$ a clause in ${\cal L}^{n}(T)$. 
Then there exists a set of clauses $S$ or-introduced from $D$ such 
that for each $E\in S$ there exists a clause $C\in T$ such that 
$C\preceq E$.
\end{theorem}

\begin{proof}
The proof is by complete mathematical induction on $n$.
It should be noted that $D$ and $S$, in the statement of the theorem, 
in the proof are indexed by $n$. 

{\em Base step (n=1)}: 
By the definition of $n$th resolution layer 
${\cal L}^{1}(T)=T$, and thus $D_{1}\in T$.
We have that $S_{1}=\{D_{1}\}$ is or-introduced from $D_{1}$ by 
the empty sequence of literals $\Omega_{1}=[]$. 
Hence, for $D_{1}\in S_{1}$ there exists a clause $D_{1}\in T$ 
such that $D_{1}\preceq D_{1}$. 

{\em Induction hypothesis (n=k)}: 
For every $1\leq i\leq k$, there exists a set of clauses 
$S_{i}$ or-introduced from $D_{i}$ by some sequence of literals 
$\Omega_{i}=[L_{1},\ldots,L_{i-1}]$ such that 
for each $E\in S_{i}$ there exists a clause 
$C\in T$ such that $C\preceq E$.

{\em Induction step (n=k+1)}: 
By the definition of $n$th resolution layer, 
$D_{k+1}$ is a resolvent of some clauses $D_{m}\in {\cal L}^{m}(T)$ 
and $D_{p}\in {\cal L}^{p}(T)$ such that $m+p=k$, $1\leq m\leq k$ and 
$1\leq p\leq k$. 
Then by Proposition \ref{PredF}, there exists a literal $L$ such that 
$D_{m}\preceq D_{k+1}\cup\{L\}$ and $D_{p}\preceq D_{k+1}\cup\{\overline{L}\}$. 

By the induction hypothesis, there exists a set of clauses 
$S_{m}$ or-introduced from $D_{m}$ by some sequence of literals 
$\Omega_{m}=[A_{1},\ldots,A_{m-1}]$ such that 
for each $E\in S_{m}$ there exists a clause $C\in T$ such that 
$C\preceq E$. 
Then by Lemma \ref{LredE}, there exists a set of clauses $S'_{m}$ 
or-introduced from $D_{k+1}\cup\{L\}$ by some sequence of literals 
$\Omega'_{m}=[A'_{1},\ldots,A'_{m-1}]$ such that 
for each $E'\in S'_{m}$ there exists a clause $C\in T$ such that 
$C\preceq E'$. 

By the induction hypothesis, there also exists a set of clauses 
$S_{p}$ or-introduced from $D_{p}$ by some sequence of literals 
$\Omega_{p}=[B_{1},\ldots,B_{p-1}]$ such that 
for each $E\in S_{p}$ there exists a clause $C\in T$ such that 
$C\preceq E$. 
Then by Lemma \ref{LredE}, there exists a set of clauses $S'_{p}$ 
or-introduced from $D_{k+1}\cup\{\overline{L}\}$ by some sequence 
of literals $\Omega'_{p}=[B'_{1},\ldots,B'_{p}]$ such that 
for each $E'\in S'_{p}$ there exists a clause $C\in T$ such that 
$C\preceq E'$. 

Then it follows from the definition of or-introduction that
$S_{k+1}=S'_{m}\cup S'_{p}$ is a set of clauses or-introduced 
>from $D_{k+1}$ by 
$\Omega_{k+1}=[L,A'_{1},\ldots,A'_{m},B'_{1},\ldots,B'_{p}]$. 
Consequently, there exists a set of clauses $S_{k+1}$ 
or-introduced from $D_{k+1}$ such that for each $E\in S_{k+1}$ 
there exists a clause $C\in T$ such that $C\preceq E$.
\end{proof}



\subsection{Expansion of Clauses}
\label{sEoC}

In the  section \ref{sIMRbOi} it was described how a reduction of
generalization can be achieved by replacing a clause by a set of clauses.
Here we show how this set of clauses equivalently can be described by a
single clause, which we call an expansion of the original clause. 
By definition, if a clause $C$ $\theta$-subsumes every clause in
a set of clauses $S$, then $C$ will also $\theta$-subsume an LGG$\theta$ of 
$S$. This leads us to our definition of expansion of clauses.
The idea of expansion of clauses was first presented by 
Idestam-Almquist \nocite{Ide93}(1993c).

\begin{definition}
Let $D$ be a clause and $\Omega$ a sequence of literals. 
Then a clause $E$ is an {\em expansion}\index{expansion} of $D$ by $\Omega$ 
if and only if $E$ is an LGG$\theta$ of a set of clauses or-introduced from 
$D$ by $\Omega$.
\end{definition}

\begin{example}
Consider the following clauses:
\[\begin{array}{l}
C=(\:p(f(x))\leftarrow p(x)\:), \\
D=(\:p(f^{3}(a))\leftarrow p(a)\:), \\
D_{1}=(\:p(f^{3}(a))\leftarrow p(f^{2}(a)),\:p(a)\:), \\
D_{2}=(\:p(f^{3}(a)),\:p(f^{2}(a)),\:p(f(a)\leftarrow p(a)\:), \\
D_{3}=(\:p(f^{3}(a)),\:p(f^{2}(a))\leftarrow p(f(a)),\:p(a)\:),$ and $\\
E=(\:p(f(x)),\:p(f^{3}(a))\leftarrow p(a),\:p(x)\:).
\end{array}\]
The set of clauses $\{D_{1},D_{2},D_{3}\}$ is or-introduced from the 
clause $D$ by $[p(f^{2}(a)),p(f(a))]$, and $E$ is an LGG$\theta$ of 
$\{D_{1},D_{2},D_{3}\}$. Consequently, $E$ is an expansion of $D$ by 
$[p(f^{2}(a)),\:p(f(a))]$.
\end{example}

Note that implication has been reduced to 
$\theta$-subsumption in the example above. 
We have $C\Rightarrow D$ and $C\not\preceq D$, but for the 
expansion $E$ of $D$ we have $C\preceq E$.

Expansion can be regarded as a transformation technique, since the expansion
of a clause is logically equivalent to the clause itself. 

\begin{theorem}
\label{TEpoe}
\index{equivalence preservation of expansion}
\index{theorem-dd@theorem \ref{TEpoe}}
{\bf (Equivalence preservation of expansion)} 
Let $D$ be a clause, and $E$ an expansion of $D$. 
Then $E\Leftrightarrow D$.
\end{theorem}

\begin{proof}
By the definition of expansion, we know that there exists a set of 
clauses $S$ or-introduced 
>from $D$ by $\Omega$ such that $E$ is an LGG$\theta$ of $S$. 
By Theorem \ref{TEpooi}, we have $\{D\}\equiv S$. 
By the definition of an LGG$\theta$, $E\preceq F$ for each $F\in S$. 
Then by Proposition \ref{PimplB}, $E\Rightarrow F$ for each $F\in S$. 
Thus $\{E\}\models S$, and consequently $E\Rightarrow D$.

We have $D\subseteq F$ for each $F\in S$. Then by the definition of an 
LGG$\theta$, we have $D\preceq E$, and by Proposition \ref{PimplB} 
$D\Rightarrow E$. Consequently, $E\Leftrightarrow D$.
\end{proof}

Below we prove that for every generalization under implication of a clause 
there exists an expansion of the clause such that the generalization under 
implication is reduced to a generalization under $\theta$-subsumption.

\begin{theorem}
\label{TRoittsbye}
\index{reduction of implication to \\$\theta$-subsumption using expansion}
\index{theorem-de@theorem \ref{TRoittsbye}}
{\bf (Reduction of implication to $\theta$-subsumption using expansion)}
Let $C$ be a clause and $D$ a non-tautological clause such that 
$C \Rightarrow D$. Then there exists an expansion $E$ of $D$ such that 
$C\preceq E$.
\end{theorem}

\begin{proof}
By Corollary \ref{CIbcur}, there exists a clause 
$D'\in {\cal L}^{n}(\{C\})$ such that $D'\preceq D$ for some $n\geq 1$. 
By Theorem \ref{TIruoi}, there
exists a set of clauses $S'$ or-introduced from $D'$ such that 
for each $F'\in S'$ we have $C\preceq F'$. Then it follows from 
Lemma \ref{LredE} that there exists a set of clauses $S$ or-introduced 
>from $D$ such that for each $F\in S$ we have $C\preceq F$. Then let $E$ 
be an LGG$\theta$ of $S$, and thus an expansion of $D$, 
and we have $C\preceq E$ by the definition of an LGG$\theta$.
\end{proof}



\subsection{Complete Expansion}
\label{sCE}

Generalizations under implication of a clause can be reduced to 
generalizations under $\theta$-subsumption of an expansion of the clause. 
We are particularly interested in expansions of clauses such that every 
generalization under implication is reduced to a generalization under 
$\theta$-subsumption of that particular expansion. 

\begin{definition}
Let $D$ be a clause, and $E$ an expansion of $D$. 
Then $E$ is a {\em complete expansion}\index{complete expansion} 
of $D$ if and only if, for every clause $C$, 
$C\preceq E$ whenever $C\Rightarrow D$.
\end{definition}

Recall that an expansion of a clause is a clause, and thus finite. 
Muggleton and Page \nocite{MP94b}(1994, page 166) has shown 
that complete expansions, which they call finite self-saturations, do 
not exist for all clauses.

\begin{theorem}
\label{TNeoce}
{\bf (Non-existence of complete expansions)}
There exist non-tautological clauses for which there exist 
no complete expansions.
\end{theorem}

The non-existence of complete expansions is due to that for some 
clauses there are infinitely many distinct generalizations 
under implication.
Because of this we turn to 
the problem of reducing every generalization under T-implication 
to a generalization under $\theta$-subsumption of a single expansion. 

\begin{definition}
Let $D$ be a clause, $E$ an expansion of $D$ and $T$ a term set of $\{D\}$. 
Then $E$ is a {\em T-complete expansion}\index{T-complete expansion} of $D$ 
w.r.t.\ $T$ if and only if, for every clause $C$, 
$C\preceq E$ whenever $C\Rightarrow_{T} D$.
\end{definition}

\begin{example}
Consider the following clauses:
\[\begin{array}{l}
C_{1}=(\:p(f(x))\leftarrow p(x)\:), \\
C_{2}=(\:p(f^{2}(y))\leftarrow p(y)\:), \\
D=(\:p(f^{4}(a))\leftarrow p(a)\:), \\
E_{1}=(\:p(f^{2}(y)),\:p(f^{4}(a))\leftarrow p(a),\:p(y)\:),$ and $\\
E_{2}=(\:p(f(x)),\:p(f^{2}(y)),\:p(f^{4}(a))\leftarrow p(a),\:p(y),\:p(x)\:).
\end{array}\]
The clauses $C_{1}$ and $C_{2}$ are proper indirect roots 
of $D$, such that $C_{1}\Rightarrow_{T} D$ and $C_{2}\Rightarrow_{T} D$. 
The clause $E_{1}$ is an expansion of $D$ by $[p(f^{2}(a))]$, and 
$E_{1}$ is an expansion of $D$ by $[p(f^{2}(a)),\:p(f^{3}(a)),\:p(f(a))]$. 
The expansion $E_{2}$ is a T-complete expansion but $E_{1}$ is not.
\end{example}

In the example above the T-complete expansion $E_{2}$ of $D$ is also 
a complete expansion of $D$. However, in contrast to complete 
expansions, T-complete expansions exist for all non-tautological 
clauses.  

\begin{theorem}
\label{TEoTce}
\index{existence of T-complete expansions}
\index{theorem-dh@theorem \ref{TEoTce}}
{\bf (Existence of T-complete expansions)} 
Let $D$ be a non-tauto\-logical clause and $T$ a term set of $\{D\}$. 
Then there exists a T-complete expansion $E$ of $D$ w.r.t.\ $T$.
\end{theorem}

\begin{proof}
By Theorem \ref{TEosLGGTs}, there exists a complete LGGT $F$ of $\{D\}$ 
w.r.t.\ $T$. 
Hence, for every clause $C$, if $C\Rightarrow_{T} D$ then $C\preceq F$. 
By the definition of a complete LGGT, we have 
$F\Rightarrow_{T} D$, and then by Corollary \ref{CRbiaTi}, $F\Rightarrow D$. 
By theorem \ref{TRoittsbye}, there exists an expansion $E$ of $D$ such that 
$F\preceq E$. 
Thus, for every clause $C$, if $C\Rightarrow_{T} D$ then $C\preceq E$, 
and consequently $E$ is a T-complete expansion of $D$ w.r.t.\ $T$.
\end{proof}

If we can compute T-complete expansions of a set of clauses 
then we can use Plotkin's algorithm for computing an LGG$\theta$ 
to compute an LGGT. From the proof of Theorem \ref{TEoTce} it follows 
that the candidate set of literals to be used to compute a T-complete 
expansion is finite. 
Since expansion is equivalence preserving we could simply test all different 
ways to expand a clause by sequences of literals from this candidate set, 
and in this way obtain a T-complete expansion. This is of course an extremely 
complex process, but at least theoretically, T-complete expansions 
and LGGTs are computable.




\section{Concluding Remarks}
\label{CR}

We have studied the problem of generalization of clauses. 
In section \ref{GoC}, we described the framework for generalization 
of clauses developed by Plotkin 
\nocite{Plo70,Plo71,Plo71b}(1970, 1971b, 1971a), which is based on 
$\theta$-subsumption. 
Implication is the most natural basis for inductive generalization. 
In section \ref{GoC}, we therefore also studied the theory of 
generalization under implication. 

The contents of section \ref{GoC} can be summarized as follows:
\begin{enumerate}
\item It is decidable whether a clause $\theta$-subsumes another clause.
\item There exists a least general generalization under $\theta$-subsumption 
(LGG$\theta$) of every finite set of clauses.
\item It is undecidable whether a clause implies another clause.
\item It is an open problem whether there exists a least general 
generalization  under implication (LGGI) of every finite set of clauses. 
\item T-implication is a strictly stronger relation between clauses than 
implication, and strictly weaker than $\theta$-subsumption, 
and T-implication can become an arbitrarily good approximation of implication 
by extending the considered term set. 
\item It is decidable whether a clause T-implies another clause. 
\item There exists a least general generalization under T-implication 
(LGGT) of every finite set of clauses. 
\end{enumerate}

In section \ref{RoItts}, we studied the difference between 
$\theta$-subsumption and implication on clauses. 
We presented our approach to find all generalizations under implication, 
by reducing implication to $\theta$-subsumption. 
This can be achieved by inverting self-resolution, and 
we described a technique for inverting resolution based on or-introduction 
of literals. We also described expansion of clauses, which summarizes 
our idea of reduction of implication to $\theta$-subsumption.

The contents of section \ref{RoItts} can be summarized 
as follows:
\begin{enumerate}
\item An expansion of a clause is an LGG$\theta$ of a set of clauses 
obtained by or-introduction from the clause. 
\item For every generalization under implication of a clause there exists 
an expansion of the clause, logically equivalent to the clause, such that 
the generalization under implication is reduced to a generalization under 
$\theta$-subsumption.
\item There exist non-tautological clauses for which there exist no 
complete expansions, which means that there are no expansions of the clauses 
such that every generalization under implication is reduced to a 
generalization under $\theta$-subsumption of the expansions. 
\item For each non-tautological clause there exists a T-complete expansion, 
which means that every generalization under T-implication of the clause 
is reduced to a generalization under $\theta$-subsumption of the expansion.
\end{enumerate}

As noted in section \ref{sCE}, T-complete expansions and LGGTs are 
computable, but such a computation is extremely costly. 
This is not surprising since our framework for generalization 
under implication 
is based on and extends Plotkin's framework for generalization 
under $\theta$-subsumption, which already suffers from complexity problems. 
In general an LGG of a set of clauses may grow exponentially 
in the number of clauses in the set \cite{MF90}. 
Even an LGG reduced under $\theta$-subsumption, which means that all 
literals that are redundant under $\theta$-subsumption are removed, 
may grow exponentially in the number of clauses \cite{Kie93}. 
% An LGG computed by Plotkin's algorithm usually includes a lot of 
% literals redundant under $\theta$-subsumption, and the cost of reducing 
% a clause by removing redundant literals grows exponentially 
% in the size of the unreduced clause \cite{GF93}. 
% Consequently, in the worst case the cost of computing a 
% reduced LGG may grow double exponentially in the number of 
% clauses.
Since an expansion of a clause is an LGG of a set of or-introduced 
clauses, the computational cost of an expansion grows exponentially in the 
number of literals used in the or-introduction. 
In the computation of a T-complete expansion a large number of literals 
may be considered, and consequently such a computation would be 
extremely costly.  

However, although Plotkin's framework for generalization under 
$\theta$-subsump\-tion is computationally expensive, it has been widely 
used as a theoretical framework. 
Then to make it practical, a number of different restrictions on the 
clausal language has been considered, 
for example $ij$-determinacy \cite{MF90}.
In a similar way we hope to find restrictions under which our here 
presented framework for generalization under implication can be 
practically useful. 

Idestam-Almquist \nocite{Ide93d,Ide93e}(1993b, 1993a) has described a 
technique to efficiently compute a restricted form of generalizations 
under implication. 
Recently, Muggleton has presented another approach 
based on generating a number of clauses, so called sub-saturants, 
which are candidates for being indirect roots, and then testing 
whether they are so or not \cite{Mug95}. 
This approach might be a way to more efficiently compute some 
generalizations under implication. 
Some approaches to learn recursive definitions 
(recursive logic programs) by generalization under implication 
have been presented \cite{LM92,ALLM94,Ide95}. 
These approaches are based on structural analysis of the given 
examples, but can theoretically be described in our framework.  

A study by Cohen \nocite{Coh95,Coh95b}(1995a, 1995b) of the 
learnability of recursive logic programs has previously been presented 
in this journal. 
In this study it was shown that a recursive logic program consisting of 
one constant-depth determinate closed $k$-ary recursive clause and one 
constant-depth determinate non-recursive clause is PAC-learnable 
given an additional ``base-case oracle'', which determines if a 
positive example is covered by the non-recursive base clause of the 
target program alone. It was also shown that generalizing this class 
of learning problem in any natural way leads to a computationally 
difficult problem. This result tells us that to efficiently learn 
more complex recursive hypotheses some extra information, such as 
rule models \cite{KW92} or program recursion schemes \cite{HN94}, 
is needed. 

The contributions of this paper are threefold. 
First, we have systematically reviewed and discussed the concepts 
relevant to generalization in a first-order setting. 
Second, we have introduced T-implication, a stronger form of 
implication which is decidable between clauses. 
Third, we have further developed previous work of the author 
\cite{Ide93} on extending Plotkin's framework for generalization 
under $\theta$-subsumption to generalization under implication. 




\acks{The author wish to thank Torkel Franz{\'{e}}n for invaluable help 
concerning the work on T-implication. 
The author also wish to thank Shan-Hwei Nienhuys-Cheng, Ronald de Wolf and 
the anonymous reviewers for a number of thoughtful comments and suggestions 
of improvements. 

This work has been supported by the Swedish Research Council for Engineering 
Sciences (TFR) and the European Community ESPRIT BRA 6020 Inductive Logic 
Programming.}



\vskip 0.2in
% \bibliography{/a/mars/home0/mars/dsv/pi/pi}
% \bibliographystyle{theapa}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Aha, Lapointe, Ling, \BBA\ Matwin}{Aha
  et~al.}{1994}]{ALLM94}
Aha, D.~W., Lapointe, S., Ling, C.~X., \BBA\ Matwin, S. \BBOP1994\BBCP.
\newblock \BBOQ Inverting implication with small training sets\BBCQ\
\newblock In {\Bem Proceedings of the Seventh European Conference on Machine
  Learning}. Springer-Verlag.

\bibitem[\protect\BCAY{Bain \BBA\ Muggleton}{Bain \BBA\ Muggleton}{1992}]{BM92}
Bain, M.\BBACOMMA\  \BBA\ Muggleton, S. \BBOP1992\BBCP.
\newblock \BBOQ Non-monotonic learning\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Inductive Logic Programming}. Academic
  Press, London.

\bibitem[\protect\BCAY{Chang \BBA\ Lee}{Chang \BBA\ Lee}{1973}]{CL73}
Chang, C.\BBACOMMA\  \BBA\ Lee, R. \BBOP1973\BBCP.
\newblock {\Bem Symbolic Logic and Mechanical Theorem Proving}.
\newblock Academic Press, London.

\bibitem[\protect\BCAY{Cohen}{Cohen}{1995a}]{Coh95}
Cohen, W. \BBOP1995a\BBCP.
\newblock \BBOQ Pac-learning recursive logic programs: Efficient
  algorithms\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 2},
  501--539.

\bibitem[\protect\BCAY{Cohen}{Cohen}{1995b}]{Coh95b}
Cohen, W. \BBOP1995b\BBCP.
\newblock \BBOQ Pac-learning recursive logic programs: Negative results\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 2},
  541--573.

\bibitem[\protect\BCAY{Gallier}{Gallier}{1986}]{Gal86}
Gallier, J.~H. \BBOP1986\BBCP.
\newblock {\Bem Logic for Computer Science - Foundations of Automatic Theorem
  Proving}.
\newblock Harper \& Row Publishers.

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

\bibitem[\protect\BCAY{Hamfelt \BBA\ Nilsson}{Hamfelt \BBA\
  Nilsson}{1994}]{HN94}
Hamfelt, A.\BBACOMMA\  \BBA\ Nilsson, J.~F. \BBOP1994\BBCP.
\newblock \BBOQ Inductive metalogic programming\BBCQ\
\newblock In {\Bem Proceedings of the Fourth International Workshop on
  Inductive Logic Programming}. Gesellschaft f{\"{u}}r Mathematik und
  Datenverarbeitung mb{H}, Bad Honnef/Bonn, Germany.

\bibitem[\protect\BCAY{Helft}{Helft}{1987}]{Hel87}
Helft, N. \BBOP1987\BBCP.
\newblock \BBOQ Inductive generalization: A logical framework\BBCQ\
\newblock In {\Bem Proceedings of the Second European Working Session on
  Learning}. Sigma Press, Wilmslow, England.

\bibitem[\protect\BCAY{Hume \BBA\ Sammut}{Hume \BBA\ Sammut}{1991}]{HS91}
Hume, D.\BBACOMMA\  \BBA\ Sammut, C. \BBOP1991\BBCP.
\newblock \BBOQ Using inverse resolution to learn relations from
  experiments\BBCQ\
\newblock In {\Bem Proceedings of the Eighth International Workshop on Machine
  Learning}. Morgan Kaufmann.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1992}]{Ide92}
Idestam-Almquist, P. \BBOP1992\BBCP.
\newblock \BBOQ Learning missing clauses by inverse resolution\BBCQ\
\newblock In {\Bem Proceedings of the International Conference on Fifth
  Generation Computer Systems 1992}. Ohmsha Publishers, Tokyo.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1993a}]{Ide93e}
Idestam-Almquist, P. \BBOP1993a\BBCP.
\newblock {\Bem Generalization of Clauses}.
\newblock Ph.D.\ thesis, Department of Computer and Systems Sciences, Stockholm
  University and Royal Institute of Technology.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1993b}]{Ide93d}
Idestam-Almquist, P. \BBOP1993b\BBCP.
\newblock \BBOQ Generalization under implication by recursive
  anti-unification\BBCQ\
\newblock In {\Bem Proceedings of the Tenth International Conference on Machine
  Learning}. Morgan Kaufmann.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1993c}]{Ide93}
Idestam-Almquist, P. \BBOP1993c\BBCP.
\newblock \BBOQ Generalization under implication by using
  or-intro\-duction\BBCQ\
\newblock In {\Bem Proceedings of the Sixth European Conference on Machine
  Learning}. Springer-Verlag.

\bibitem[\protect\BCAY{Idestam-Almquist}{Idestam-Almquist}{1995}]{Ide95}
Idestam-Almquist, P. \BBOP1995\BBCP.
\newblock \BBOQ Efficient induction of recursive definitions by structural
  analysis of saturations\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Workshop on Inductive
  Logic Programming}. Department of Computer Science, Katholieke Universiteit
  Leuven, Belgium.

\bibitem[\protect\BCAY{Kietz}{Kietz}{1993}]{Kie93}
Kietz, J.-U. \BBOP1993\BBCP.
\newblock \BBOQ A comparative study of structural most specific generalizations
  used in machine learning\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Proceedings of the Third International
  Workshop on Inductive Logic Programming}. J. Stefan Institute, Ljubljana,
  Slovenia.

\bibitem[\protect\BCAY{Kietz \BBA\ Wrobel}{Kietz \BBA\ Wrobel}{1992}]{KW92}
Kietz, J.-U.\BBACOMMA\  \BBA\ Wrobel, S. \BBOP1992\BBCP.
\newblock \BBOQ Controlling the complexity of learning in logic through
  syntactic and task-oriented models\BBCQ\
\newblock In Muggleton, S.\BED, {\Bem Inductive Logic Programming}. Academic
  Press, San Diego, California.

\bibitem[\protect\BCAY{Kowalski}{Kowalski}{1970}]{Kow70}
Kowalski, R. \BBOP1970\BBCP.
\newblock \BBOQ The case for using equality axioms in automatic
  demonstration\BBCQ\
\newblock In {\Bem Symposium on Automatic Demonstration, Lecture notes in
  Mathematics, Vol. 125}. Springer-Verlag.

\bibitem[\protect\BCAY{Lapointe \BBA\ Matwin}{Lapointe \BBA\
  Matwin}{1992}]{LM92}
Lapointe, S.\BBACOMMA\  \BBA\ Matwin, S. \BBOP1992\BBCP.
\newblock \BBOQ Sub-unification: A tool for efficient induction of recursive
  programs\BBCQ\
\newblock In {\Bem Proceedings of the Ninth International Conference on Machine
  Learning}. Morgan Kaufmann.

\bibitem[\protect\BCAY{Lavra\v{c} \BBA\ De~Raedt}{Lavra\v{c} \BBA\
  De~Raedt}{1995}]{LD95}
Lavra\v{c}, N.\BBACOMMA\  \BBA\ De~Raedt, L. \BBOP1995\BBCP.
\newblock \BBOQ Inductive logic programming: A survey of {European}
  research\BBCQ\
\newblock {\Bem AI Communications}, {\Bem 8\/}(1), 3--19.

\bibitem[\protect\BCAY{Lavra\v{c} \BBA\ D\v{z}eroski}{Lavra\v{c} \BBA\
  D\v{z}eroski}{1994}]{LD94}
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, C. \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}]{Llo87}
Lloyd, J.~W. \BBOP1987\BBCP.
\newblock {\Bem Foundations of Logic Programming}.
\newblock Springer-Verlag.
\newblock Second edition.

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

\bibitem[\protect\BCAY{Muggleton}{Muggleton}{1990}]{Mug90}
Muggleton, S. \BBOP1990\BBCP.
\newblock \BBOQ Inductive logic programming\BBCQ\
\newblock In {\Bem Proceedings of the Workshop on Algorithmic Learning Theory}.
  Ohmsha Publishers, Tokyo.

\bibitem[\protect\BCAY{Muggleton}{Muggleton}{1991}]{Mug91}
Muggleton, S. \BBOP1991\BBCP.
\newblock \BBOQ Inductive logic programming\BBCQ\
\newblock {\Bem New Generation Computing Journal}, {\Bem 8\/}(4), 295--318.

\bibitem[\protect\BCAY{Muggleton}{Muggleton}{1992}]{Mug92}
Muggleton, S. \BBOP1992\BBCP.
\newblock \BBOQ Inverting implication\BBCQ\
\newblock In {\Bem Proceedings of the Second International Workshop on
  Inductive Logic Programming}. ICOT Technical Memorandum TM-1182.

\bibitem[\protect\BCAY{Muggleton}{Muggleton}{1993}]{Mug93}
Muggleton, S. \BBOP1993\BBCP.
\newblock \BBOQ Inductive logic programming: Derivations, successes and
  shortcomings\BBCQ\
\newblock In {\Bem Proceedings of the Sixth European Conference on Machine
  Learning}. Springer-Verlag.

\bibitem[\protect\BCAY{Muggleton}{Muggleton}{1995}]{Mug95}
Muggleton, S. \BBOP1995\BBCP.
\newblock \BBOQ Inverse entailment and {Progol}\BBCQ\
\newblock {\Bem New Generation Computing Journal}, {\Bem 13}.

\bibitem[\protect\BCAY{Muggleton \BBA\ Buntine}{Muggleton \BBA\
  Buntine}{1988}]{MB88}
Muggleton, S.\BBACOMMA\  \BBA\ Buntine, W. \BBOP1988\BBCP.
\newblock \BBOQ Machine invention of first-order predicates by inverting
  resolution\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Conference on Machine
  Learning}. Morgan Kaufmann.

\bibitem[\protect\BCAY{Muggleton \BBA\ De~Raedt}{Muggleton \BBA\
  De~Raedt}{1994}]{MD94}
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,20}, 629--679.

\bibitem[\protect\BCAY{Muggleton \BBA\ Feng}{Muggleton \BBA\ Feng}{1990}]{MF90}
Muggleton, S.\BBACOMMA\  \BBA\ Feng, C. \BBOP1990\BBCP.
\newblock \BBOQ Efficient induction of logic programs\BBCQ\
\newblock In {\Bem Proceedings of the Workshop on Algorithmic Learning Theory}.
  Ohmsha Publishers, Tokyo.

\bibitem[\protect\BCAY{Muggleton \BBA\ Page}{Muggleton \BBA\
  Page}{1994}]{MP94b}
Muggleton, S.\BBACOMMA\  \BBA\ Page, D. \BBOP1994\BBCP.
\newblock \BBOQ Self saturation of definite clauses\BBCQ\
\newblock In {\Bem Proceedings of the Fourth International Workshop on
  Inductive Logic Programming}. Gesellschaft f{\"{u}}r Mathematik und
  Datenverarbeitung mb{H}, Bad Honnef/Bonn, Germany.

\bibitem[\protect\BCAY{Niblett}{Niblett}{1988}]{Nib88}
Niblett, T. \BBOP1988\BBCP.
\newblock \BBOQ A study of generalization in logic programs\BBCQ\
\newblock In {\Bem Proceedings of the Third European Working Session on
  Learning}. Pitman.

\bibitem[\protect\BCAY{Nienhuys-Cheng \BBA\ de~Wolf}{Nienhuys-Cheng \BBA\
  de~Wolf}{1995}]{NW95}
Nienhuys-Cheng, S.-H.\BBACOMMA\  \BBA\ de~Wolf, R. \BBOP1995\BBCP.
\newblock \BBOQ The subsumption theorem in inductive logic programming: Facts
  and fallacies\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Workshop on Inductive
  Logic Programming}. Department of Computer Science, Katholieke Universiteit
  Leuven, Belgium.

\bibitem[\protect\BCAY{Plotkin}{Plotkin}{1970}]{Plo70}
Plotkin, G.~D. \BBOP1970\BBCP.
\newblock \BBOQ A note on inductive generalization\BBCQ\
\newblock In Meltzer, B.\BBACOMMA\  \BBA\ Michie, D.\BEDS, {\Bem Machine
  Intelligence}, \lowercase{\BVOL}~5, \BPGS\ 153--163. Edinburgh University
  Press.

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

\bibitem[\protect\BCAY{Plotkin}{Plotkin}{1971b}]{Plo71}
Plotkin, G.~D. \BBOP1971b\BBCP.
\newblock \BBOQ A further note on inductive generalization\BBCQ\
\newblock In Meltzer, B.\BBACOMMA\  \BBA\ Michie, D.\BEDS, {\Bem Machine
  Intelligence}, \lowercase{\BVOL}~6, \BPGS\ 101--124. Edinburgh University
  Press.

\bibitem[\protect\BCAY{Quinlan}{Quinlan}{1986}]{Qui86}
Quinlan, J.~R. \BBOP1986\BBCP.
\newblock \BBOQ Induction of decision trees\BBCQ\
\newblock {\Bem Machine Learning Journal}, {\Bem 1\/}(1), 81--106.

\bibitem[\protect\BCAY{Robinson}{Robinson}{1965}]{Rob65}
Robinson, J.~A. \BBOP1965\BBCP.
\newblock \BBOQ A machine-oriented logic based on the resolution
  principle\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 12\/}(1), 23--41.

\bibitem[\protect\BCAY{Rouveirol}{Rouveirol}{1992}]{Rou92}
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}. Academic
  Press, San Diego, California.

\bibitem[\protect\BCAY{Rouveirol \BBA\ Puget}{Rouveirol \BBA\
  Puget}{1989}]{RP89}
Rouveirol, C.\BBACOMMA\  \BBA\ Puget, J.-F. \BBOP1989\BBCP.
\newblock \BBOQ A simple solution for inverting resolution\BBCQ\
\newblock In {\Bem Proceedings of the Fourth European Working Session on
  Learning}. Pitman.

\bibitem[\protect\BCAY{Schmidt-Schauss}{Schmidt-Schauss}{1988}]{Sch88}
Schmidt-Schauss, M. \BBOP1988\BBCP.
\newblock \BBOQ Implication of clauses is undecidable\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 59}, 287--296.

\bibitem[\protect\BCAY{Slagle, Chang, \BBA\ Lee}{Slagle et~al.}{1969}]{SCL69}
Slagle, J.~R., Chang, C.~L., \BBA\ Lee, R. C.~T. \BBOP1969\BBCP.
\newblock \BBOQ Completeness theorems for semantic resolution in
  consequence-finding\BBCQ\
\newblock In {\Bem Proceedings of the First International Joint Conference on
  Artificial Intelligence}. Morgan Kaufmann, Los Altos, California.

\bibitem[\protect\BCAY{Wirth}{Wirth}{1989}]{Wir89}
Wirth, R. \BBOP1989\BBCP.
\newblock \BBOQ Completing logic programs by inverse resolution\BBCQ\
\newblock In {\Bem Proceedings of the Fourth European Working Session on
  Learning}. Pitman.

\end{thebibliography}


\end{document}










