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

\jairheading{10}{1999}{169-198}{9/98}{3/99}
\ShortHeadings{Cooperation between Top-Down and Bottom-Up Theorem Provers}
{Fuchs \& Fuchs}
\firstpageno{169}

\begin{document}

\title{Cooperation between Top-Down and Bottom-Up\\Theorem Provers}

\author{\name Dirk Fuchs \email dfuchs@informatik.uni-kl.de \\
       \addr Fachbereich Informatik, Universit\"at Kaiserslautern\\
       67663 Kaiserslautern, Germany
       \AND
       \name Marc Fuchs \email fuchsm@informatik.tu-muenchen.de \\
       \addr Fakult\"at f\"ur Informatik, TU M\"unchen \\
       80290 M\"unchen, Germany}

% For research notes, remove the comment character in the line below.
% \researchnote

\maketitle

%%% MACROS %%%
\def\fact{\lambda}
\def\nat{\mbox{I\hspace{-0.4ex}N}}
\def\zet{\mbox{\sf Z\hspace{-1.7ex} Z}}
\def\real{\mbox{I\hspace{-0.4ex}R}}
\def\otter{{\sc Otter}}
\def\dicode{{\sc DiCoDe}}
\def\code{{\sc CoDe}}
\def\discount{{\sc Discount}}
\def\teamwork{{\sc Teamwork}}
\def\spass{{\sc Spass}}
\def\setheo{{\sc Setheo}}
\def\var{{\cal V}}
\def\fsym{{\cal F}}
\def\monus{\stackrel{.}{-}}
\def\lcl#1{{\tt LCL#1-1}}
\def\grp#1#2{{\tt GRP#1-#2}}
\def\cat#1#2{{\tt CAT#1-#2}}
\def\col#1#2{{\tt COL#1-#2}}
\def\rng#1#2{{\tt RNG#1-#2}}
\def\num#1#2{{\tt NUM#1-#2}}
\def\rob#1#2{{\tt ROB#1-#2}}
\def\lda#1#2{{\tt LDA#1-#2}}
\def\hen#1#2{{\tt HEN#1-#2}}
\def\boo#1#2{{\tt BOO#1-#2}}
%%% ------ %%%
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{example}{Example}[section]

\input{epsf}

\hyphenation{Kaisers-lautern heu-ris-tic heu-ris-tics}

\setlength{\parskip}{0.5ex plus 0.5ex minus 0.3ex}

\newcommand{\ng}{\mbox{\raisebox{.2ex}{\footnotesize $\sim$}}}

%%%% ABSTRACT %%%%

\begin{abstract}
Top-down and bottom-up theorem proving approaches each have specific advantages and disadvantages.
Bottom-up provers profit from strong redundancy control but suffer from the lack of goal-orientation,
whereas top-down provers are goal-oriented but often have weak calculi when their proof lengths are considered.
In order to integrate both approaches, we try to achieve cooperation between a top-down
and a bottom-up prover in two different ways: 
The first technique aims at supporting a bottom-up with a top-down prover. A top-down prover
generates subgoal clauses, they are then processed by a bottom-up prover.  The second technique
deals with the use of bottom-up generated lemmas in a top-down prover.
We apply our concept to the areas of model elimination and superposition.
We discuss the ability of our techniques to shorten proofs as well
as to reorder the search space in an appropriate manner. Furthermore,
in order to identify subgoal clauses and lemmas which are actually relevant for the proof task,
we develop methods for a relevancy-based filtering.
Experiments with the provers \setheo\ and \spass\ performed in the problem library TPTP 
reveal the high potential of our cooperation approaches.
\end{abstract}


\section{Introduction}
Automated deduction is---at its lowest level---a search problem that spans huge search spaces.
In
the past many different calculi have been developed in order to cope with problems
from the area of automated theorem proving. Essentially, for first-order theorem proving
two main paradigms for 
calculi are in use: {\em Top-down calculi\/} like {\em model elimination}
\shortcite<ME, >{Lov68,Lov78}
 attempt to recursively break down and transform a goal into
 subgoals that can
finally be proven immediately with the axioms or with assumptions made during the proof.
{\em Bottom-up calculi\/} like {\em superposition} \shortcite<e.g.,>{BG94}
go the other way by
producing logic consequences from the input set until an obvious inconsistency
is derived.

When comparing results of various provers \shortcite<e.g.,>{SS97} it is obvious that provers based on different
paradigms often behave quite differently. There are problems where bottom-up theorem
provers perform considerably well, but top-down provers poorly, and vice versa. The main reason
for this is that bottom-up provers often suffer from the lack of goal-orientation of their
search, but profit from their strong redundancy control mechanisms. In contrast, top-down provers
profit from their goal-orientation but suffer from insufficient redundancy control. This
 entails
long proof lengths for many problems \shortcite<e.g.,>{LMG94b}.
Therefore, a topic that has come into the focus of research is the integration of both approaches.
Specifically, cooperation between theorem provers \shortcite<e.g.,>{CMM90,Sch94,De95,BH95,B96,WF97,Fu98RTA,Fu98JELIA} based on top-down and bottom-up principles appears
to be promising because by exchanging information each approach can profit from the
other. It is also possible to modify calculi or provers which work according to one paradigm
so as to introduce aspects of the other paradigm into it. This, however, requires a lot of
implementational effort to modify the provers, whereas our approach does not require changes
of the provers but only changes of their input. We can hence employ arbitrary
state-of-the-art provers.

Information that is well-suited for improving the performance of top-down provers 
are lemmas deduced by bottom-up provers. 
These
lemmas are added to the input of a top-down prover and can help to shorten the proof length by
immediately solving subgoals. Normally, the employed proof procedures
can significantly profit from the proof length reduction obtained.
The use of lemmas, however, also imports additional redundancy into the
calculus. This means that an unbounded use of bottom-up generated lemmas without using techniques for 
choosing only {\em relevant\/} lemmas (i.e.\ lemmas which lead to a reduction of the
search effort to enumerate a proof) is not sensible.
In this article, in contrast to other approaches which generate lemmas
dynamically during the proof run \shortcite{AS92,AL97}, we want to employ
a bottom-up prover for generating lemmas in a preprocessing phase.
After the generation of a pool of {\em lemma candidates\/} relevant lemmas
are selected from this pool
and the formula to be refuted is augmented by these bottom-up generated formulas.

The second main aspect that we consider is top-down/bottom-up integration by transferring information
from a top-down prover to a bottom-up prover \shortcite<e.g.,>{Fu98AISC}. Our approach is to transfer top-down generated {\em subgoal clauses\/}---which essentially represent a transformation of an original goal clause into
subgoals---to a bottom-up prover and to augment its input by these clauses.
This introduces a goal-oriented component into a
bottom-up prover which can enable it to solve proof problems considerably faster.
However, as is the case with lemmas, an unbounded transfer of subgoal clauses is not
sensible. Thus, we generate again subgoal clauses in a preprocessing phase and
integrate only some of these clauses into the input set of a bottom-up prover.
This necessitates techniques for {\em selecting relevant subgoal clauses\/}, i.e.\ 
techniques for selecting 
a set of subgoal clauses which can decrease the search effort of a 
bottom-up prover in order to find a proof.

In order to examine this kind of top-down/bottom-up integration
we restrict ourselves to the bottom-up superposition calculus and the top-down connection tableau calculus.
These calculi are very important since they are the basis for many high-performance theorem provers.
For instance, the bottom-up provers \spass\ \shortcite{WGR96} and Gandalf \shortcite{Ta97} that were
most successful in recent proving competitions employ superposition and ordered paramodulation,
respectively. The connection tableau calculus (or its restriction model elimination) is also the
basis for very successful top-down provers, e.g., \setheo\ \shortcite{MI97} or METEOR \shortcite{AL91}.
In our opinion the concepts introduced for superposition and the connection tableau calculus can rather
easily be transferred to other bottom-up and top-down calculi. Hence, the choice of these two
calculi surely is justified.

The article is organized as follows.
We start with a brief overview of superposition and model elimination (Section \ref{framework}).
Moreover, we discuss strengths and weaknesses of the
calculi in more detail and introduce our approach for combining the strengths of
both calculi. In Section \ref{sgclauses} we address
effects of the integration of ME subgoal clauses into the search state of a superposition-based
prover. Furthermore, we describe two variants of a relevancy-based filtering of subgoal
clauses. Section \ref{lemmas} deals with the use of bottom-up generated lemmas.
We discuss in detail the ability of the produced clauses
in order to help decrease proof lengths for refuting a given set of clauses 
as well as to reorder the search
space in an appropriate manner. Based on this discussion, we introduce
several relevancy measures.
In Section \ref{experimente}, an experimental study conducted with the high-performance theorem provers 
\setheo\ and \spass\ reveals the potential of our techniques. We have chosen these systems
in order to show that our concept can easily be integrated into existing systems and is even
able to improve on the performance of very powerful provers. Finally, in Section \ref{disc} an
overview of related approaches for top-down/bottom-up integration concludes the article.

% -------------------------------------------------------------------------------------------------
\section{A Framework for Coupling Top-Down and Bottom-Up Provers}
\label{framework}
In the following, we introduce typical representatives of top-down and bottom-up calculi and
discuss their strengths and weaknesses in detail. After that, we sketch the basics of our
methodology in order to combine these calculi.

\subsection{Automated Theorem Proving with Superposition and Model Elimination}
The general problem in first-order theorem proving is 
to show the inconsistency of a set $\cal C$ of clauses. A clause is a set of literals.
As already discussed, theorem provers usually utilize either top-down or bottom-up calculi for accomplishing this task. 

Typically, a bottom-up calculus contains several inference rules
which can be applied to a set of clauses that constitute the search state.
Generally, the inference rules can be divided into two classes: {\em Expansion\/} inference rules permit
the generation of new clauses and {\em contraction\/} inference rules delete clauses or replace them by
others. The most popular bottom-up calculus is the {\em resolution} calculus \cite{Rob65}. There, the expansion rules
are resolution and factoring. The resolution calculus can be extended with contraction rules, e.g.\ the deletion of tautologies.
If equality is involved in a problem it is sensible to employ the superposition calculus \shortcite{BG94},
which extends resolution with specific rules suitable for handling equations. The expansion rules of
the superposition calculus are superposition, equality resolution, and equality factoring. Again,
additional contraction rules such as tautology deletion, subsumption, condensing, and rewriting can be employed.
It is to be emphasized that for our study we employ the version of the superposition calculus introduced
by \shortciteA{BG94}. Specifically this entails that factoring is only applied to positive literals.


A bottom-up theorem prover usually maintains 
a set~${\cal F}^P$
of so-called {\em potential\/} or {\em passive  clauses\/}
from which it selects and removes one clause~$C$ at a time.
This clause is put into the set~${\cal F}^A$ of {\em activated clauses\/}.
Activated clauses are, unlike potential clauses, allowed to produce new
clauses via the application of some inference rules. The inferred new
clauses are put into~${\cal F}^P$.
Initially, ${\cal F}^A = \emptyset$ and ${\cal F}^P = \cal C$.
The indeterministic selection or {\em activation step\/} is realized
by heuristic means.
To this end, a heuristic~$\cal H$ associates
a natural number $\omega_C \in \nat$ with each $C \in {\cal F}^P$,
and the $C\in {\cal F}^P$ with the smallest
weight~$\omega_C$ is selected.
An important property of heuristics is their {\em fairness}. A heuristic is called fair
if it selects potential clauses in such a manner that no clause remains passive infinitely long.
Usually the fairness of the used heuristic implies that the prover is complete, i.e.\
it can derive the empty clause when obtaining an inconsistent input set (provided the underlying calculus
is complete).

The main strength of bottom-up calculi and provers is their strong redundancy control. On the one hand,
many inferences which are definitely unnecessary in a proof, e.g.\ inferences involving tautologies, are
omitted. On the other hand, contraction  inference rules like subsumption avoid the
repetition of expansion inferences involving the same (or more instantiated) clauses. A big
disadvantage of bottom-up calculi is their lack of goal-orientation. Because certain inferences are favored over others due to the fixed search strategy and the
heuristic weight of the clauses part of it, it might be the case that for a very long time only clauses  which are not part of any proof are enumerated.


Model elimination is a typical top-down  calculus which we shall introduce in the form            
of the
{\em connection tableau calculus} $(CTC)$ \shortcite{LMG94b}.
In order to introduce $CTC$ we want to start with
the basic (free variable) tableau calculus \shortcite<e.g.,>{Fit96} for clauses.
A tableau $T$ for $\cal C$ is a tree whose
non-root nodes are labeled with literals and that fulfills the condition:
If the immediate successor
nodes $v_1,\ldots,v_n$ of a node $v$ of $T$ are labeled with literals $l_1, \ldots, l_n$,
then the clause $\{l_1,\ldots,l_n\}$ ({\em tableau clause}) is an instance of a
clause in $\cal C$. In the tableau calculus two inference rules are used,
namely the {\em
expansion} and the {\em reduction} rule \shortcite<e.g.,>{Fit96}. An application of the
expansion rule means selecting a clause from $\cal C$ and attaching the literals
of a variant of it
to a {\em subgoal} $s$ which is a literal at the leaf of an {\em open} branch (a
branch that does not contain
two complementary literals). Tableau reduction closes a branch by unifying a
subgoal $s$ with the complement of a literal $r$ (denoted by $\sim r$) on the same
branch, and applying
the substitution to the whole tableau.

Connection tableau calculi work on connected tableaux. A tableau is called {\em
connected} or a {\em connection tableau} if each inner node $v$ (non-leaf node)
which is labeled with literal $l$ has a leaf node $v^\prime$ among its immediate
successor nodes that is labeled with a literal $l^\prime$ complementary to $l$.
The inference rules are {\em start}, {\em extension}, and {\em reduction}.
The start rule is always the first inference step of a derivation.
It permits a tableau expansion that can only be applied to
a trivial tableau, i.e.\  one consisting of only one node. Note that the start rule 
can be restricted to so-called {\em start relevant\/} clauses without 
causing incompleteness.  Start relevancy of a clause is defined as follows.
If ${\cal C}$ is an unsatisfiable set of clauses, we call $S\in {\cal C}$ start relevant if
there is a satisfiable subset ${\cal C}^\prime\subset {\cal C}$ such that ${\cal C}^\prime\cup \{S\}$ is
unsatisfiable.  Since the set of negative clauses contains at least one start relevant clause, 
we also consider a restricted calculus which only employs negative clauses for the start 
expansion ($CTC_{{\em neg}}$). The reduction rule is the same as in the conventional tableau calculus.
Extension is a combination of expansion and reduction. It is performed by
selecting a subgoal $s$ in the tableau $T$, applying an
expansion step to $s$, and immediately performing a reduction step with $s$ and
one of its newly created successors.
Note that in the area of Horn clauses it is sufficient to employ start and extension,
i.e.\ the reduction inference is unnecessary \shortcite<e.g.,>{AL94}. Thus, we assume that we use 
versions of $CTC$ or $CTC_{{\em neg}}$ that do not employ reduction steps in the area
of Horn clauses.

$CTC$ or $CTC_{{\em neg}}$ do not have specific inference rules for handling equality. Instead,
when dealing with equality, the axiomatization must be extended by the
reflexivity, symmetry, transitivity, and substitution axioms of the equality symbol.
Indeed, the use of an axiomatic form of equality is in no sense optimal. But it is very difficult 
to develop methods for using built-in equality in tableau calculi that yield convincing results 
in practice.

If a subgoal $s$ becomes (after some inferences) head of a closed (sub-)tableau we call 
the obtained substitution a {\em solution} of $s$.

The notion of a tableau derivation and a search tree is important:
We say $T \vdash T^\prime$ if (and only if) tableau $T^\prime$ can be derived
from $T$ by applying a start rule if $T$ is the trivial tableau, or by an
extension/reduction rule to a subgoal in $T$. 
The connection tableau calculus is not (proof) confluent.
In order to
show the unsatisfiability of a clause set $\cal C$, a search tree, given as follows,
has to be examined in a {\em fair\/} way (each node of the tree must be visited after
a finite amount of time) until a closed tableau occurs.
A {\em search tree} $\cal
T$ defined by a calculus and a set of clauses $\cal C$ is given by a tree whose root is labeled with
the trivial tableau. Every inner node in $\cal T$
labeled with tableau $T$ has as immediate successors the nodes from the maximal set 
$\{v_1,\ldots,v_n\}$, where $v_i$ is labeled with $T_i$ and
$T \vdash T_i$, $1
\leq i \leq n$.

Since not only the number of proof objects
but also their size increases during the proof process, explicit tableaux
enumeration procedures that construct all tableaux in $\cal T$ in a breadth-first
manner are not reasonable. Hence, implicit enumeration procedures 
that apply {\em consecutively bounded iterative deepening search with
backtracking} \shortcite{Korf1985} are normally used. 
In this approach iteratively larger finite initial parts of the
search tree $\cal T$ are explored with depth-first search.
A finite
segment is normally defined by a so-called {\em completeness bound\/} (which poses structural
restrictions on the tableaux which are allowed in the current segment, see below)
and a fixed natural number, a so-called
{{\em resource\/}}.
Iterative deepening is performed by starting with a basic resource value
$n \in \nat$ and
iteratively increasing $n$ until a proof is found within the finite initial segment of
$\cal T$ defined by one bound and $n$.
Prominent examples for completeness bounds are the {\em depth bound\/}, {\em inference bound\/}, and 
{\em weighted-depth bound}.

The depth bound limits the maximal depth of inner nodes (non-leaf nodes) in a tableau
where the current resource $n$ is the maximal depth permitted
(the root node has depth 0).
In practice, the depth bound is
quite successful \shortcite{LMG94b,Har96} but it suffers from the large increase of the
segment (defined by a resource $n$) caused by an increase of $n$.
The inference bound allows a level by level
exploration of the search tree \cite<e.g.,>{Sti88}.
In comparison with the depth bound, the inference bound makes a smooth increase of the
 search space possible, but it is inferior to the depth bound in practice.
In order to combine the advantages of the depth and the inference bound, the weighted-depth
bound was introduced by \shortciteA{MI97}. This bound describes a class of possible bounds
that restrict the tableau depth and the number of inferences allowed
to infer a specific tableau.

 %The configuration used within the prover \setheo\ \shortcite<see>{MI97} has
%proven to be quite successful.

Goal-orientation of $CTC$, as our typical top-down calculus, is given by the connectedness condition.
This condition entails that every literal in a tableau bears a relation to the start clause. The set of possible
start clauses can normally be restricted to quite a small set of clauses which
are sufficient in order to guarantee completeness\ \shortcite<e.g.,>{MI97}, e.g.\ the set of
negative clauses as already mentioned. Thus, only certain descendants having a connection to a start
(goal) clause are enumerated. A main problem of proofs with $CTC$ is that in general they are rather
long. In fact, $CTC$ is among the weakest calculi when the lengths of existing proofs are considered. Therefore, \shortciteA{LMG94b} proposed extensions of $CTC$
which are based on a controlled integration of the {\em cut rule\/}.
These extensions can also be seen as restricted lemma mechanisms.
A further problem is that often during the search
tableaux with the same or subsumed subgoals occur repeatedly. 
There are some extensions of the calculus proposed to overcome such problems.
E.g., by \shortciteA{LMG94b} a restricted subsumption concept and
by \shortciteA{AS92} caching techniques have been introduced. 


\subsection{Achieving Cooperation by Preprocessing and Input Augmentation}
\label{frameworkPreproc}
Our approach  of integrating top-down and bottom-up provers by cooperation is characterized by {\em
preprocessing\/} and {\em input augmentation}. Henceforth, let $\cal C$ be the initial clause set whose
inconsistency should be shown. In the preprocessing phase the bottom-up superposition prover generates a
set of clauses ${\cal C}_{BU}$ such that ${\cal C}\models {\cal C}_{BU}$. Analogously, we extract from a
certain number of proof attempts of the ME prover a clause set ${\cal C}_{TD}$ such that
${\cal C}\models {\cal C}_{TD}$. Then, the input set ${\cal C}$ of the superposition prover is
augmented by ${\cal C}_{TD}$, and the input of the ME prover with ${\cal C}_{BU}$. 
After that both provers can proceed to work in parallel. Figure \ref{fig::preproc} displays this
kind of cooperation that is essentially based on a sequential concatenation of both provers.
The approach can be seen as a specific instantiation of the general cooperation approach TECHS
\shortcite{DF98}.

Since the superposition prover works on a search state which contains a set of clauses, it is very easy to
generate a set of valid clauses in a preprocessing phase. A very simple method is to perform a fixed
number $i$ of activation steps and to generate the clause sets ${\cal F}^{A,i}$ and ${\cal F}^{P,i}$ of
active and passive clauses. Then, we select all {\em facts}, i.e.\ positive unit clauses, from ${\cal F}^{A,i}$. Since the
inferences of a superposition-based prover are sound, it produces only logic consequences of ${\cal C}$.
As we shall explain in Section \ref{lemmas} in more detail, it is not sensible to add all generated positive units to the input of
the top-down prover, i.e.\ to set ${\cal C}_{BU} = \{C:C\mbox{ is a fact}, C\in {\cal F}^{A,i}\}$. However, it is wise
to select only some units with a function $\varphi_{BU}$, i.e.\ ${\cal C}_{BU} = \varphi_{BU}(\{C:C\mbox{ is a fact},
C\in {\cal F}^{A,i}\})$.

\begin{figure*}
\hspace{3.5cm}
 \epsfxsize70mm
\epsfbox{coopbildJAIR.eps}
\caption{\label{fig::preproc}Cooperation between a  top-down and a bottom-up prover}
\end{figure*}


Because connection tableau-based provers have a search state which contains
deductions (tableaux) instead of clauses, it is at first sight not obvious how to extract valid clauses
from such a search state which will be well-suited for a superposition-based prover. A common method in
order to extract valid clauses is to employ lemma mechanisms of ME provers.
Assume that a literal $s$ is a label of the root node of a closed subtableau $T^s$. Let
$l_1,\ldots,l_n$ be the literals that are used in reduction steps for closing $T^s$ and that are
outside of $T^s$. Then, the clause $\{\sim s,\sim l_1,\ldots,\sim l_n\}$
may be derived as a new lemma (since it is a logical consequence of the tableau clauses
in $T^s$). Such a lemma could be transferred to a bottom-up prover. As appealing as this idea
sounds, it has some severe restrictions: Such lemmas usually are, e.g.\ due to instantiations which 
were previously needed to close
other branches, not as general as they could be. Hence, often they cannot be used in inferences,
and especially not in contracting inferences
 which are very important for bottom-up provers. Since these clauses are generated during the
proof run in a rather unsystematic way they do not really introduce much goal-orientation
and hence do not make use of the advantages of the search scheme typical for ME.

The concept of subgoal clauses permits the generation of clauses derived by inferences
involving a proof goal:


\begin{definition}[subgoal clause, subgoal clause set]\ 

{\em
\begin{enumerate}
\item Let ${\cal C}$ be a set of clauses, let $T$ be a tableau for ${\cal C}$. A {\em subgoal clause\/} $S_T$ regarding $T$ is the clause $S_T=
\{l_1,\ldots, l_n\}$, where the literals $l_i$ are the subgoals of the tableau $T$.
\item Let $B$ be a bound, $n\in\nat$ be a resource, and ${\cal C}$ be a set of clauses.\\
If $CTC$ is used, the {\em subgoal clause set\/} ${\cal S}^{B,n,{\cal C}}$ w.r.t.\ $B$, $n$, and ${\cal C}$,
is defined by ${\cal S}^{B,n,{\cal C}} = \{S_T: T$ is a tableau in the initial segment of the search tree 
for ${\cal C}$ and $CTC$ that is defined by $B$ and $n\}\setminus {\cal C}$.\\
If $CTC_{{\em neg}}$ is in use, the {\em subgoal clause set\/} ${\cal S}^{B,n,{\cal C}}_{{\em neg}}$ is the
set 
${\cal S}^{B,n,{\cal C}}_{{\em neg}}=\{S_T:S_T\in {\cal S}^{B,n,{\cal C}}$, the start expansion
of $T$
is performed with a negative clause$\}$.
\end{enumerate}}
\end{definition}

Note that subgoal clauses are valid clauses, i.e.\ logical consequences of the initial clause set.
The following example illustrates our notion of subgoal clauses.

\begin{example}
{\em 
Let ${\cal C}=\{\{\neg g\}, \{\neg p_1,\ldots,\neg p_n,g\}, \{\neg q_1,\ldots,\neg q_m,g\}\}$.
Then,
$\{\neg p_1,\ldots,\neg p_n\}$ is the subgoal clause $S_T$ belonging to the tableau
obtained when extending the goal $\neg g$ with the clause $\{\neg p_1,\ldots,\neg p_n, g\}$.
If we employ ${\cal B}= \mbox{inference bound } ({\em Inf\/})$ and resource $k=2$, then ${\cal S}^{{\cal B},k,{\cal
C}} = {\cal
S}^{{\cal B},k,{\cal C}}_{{\em neg}} =
\{\{\neg p_1,\ldots,\neg p_n\},\{\neg q_1,\ldots,\neg q_m\}\}$. 
}
\end{example}


A subgoal clause $S_T$ represents a transformation of an original goal clause (which is the
start clause of the tableau $T$) into new
subgoals realized by the deduction which led to the tableau $T$. The set
${\cal S}^{{\em Inf\/},k,{\cal C}}$ is the set
of all possible goal transformations into subgoal clauses within $k$ inferences if we consider {\em
all input clauses\/} to be goal clauses, the set ${\cal S}^{{\em Inf\/},k,{\cal C}}_{{\em neg}}$ is the set of
all possible goal transformations into subgoal clauses within $k$ inferences if we only consider
{\em the negative clauses\/} to be goal clauses.
More exactly, ${\cal S}^{{\em Inf\/},k,{\cal C}}$ is the closure
of all (goal) clauses w.r.t.\ (a fixed number $k$ of) extension and reduction steps, ${\cal S}^{{\em Inf\/}, 
k,{\cal C}}_{{\em neg}}$ is the closure
of all negative (goal) clauses w.r.t.\ $k$ extension and reduction steps.

In order to couple an ME and a superposition prover, we generate in the preprocessing phase 
with the inference bound and a
fixed resource $k>1$ either the set ${\cal S}^{{\em Inf\/},k,{\cal C}}$ 
or the set ${\cal S}^{{\em Inf\/}, k,{\cal C}}_{{\em neg}}$, 
depending on whether $CTC$ or $CTC_{{\em neg}}$ is used.
It is not sensible to set ${\cal C}_{TD} = {\cal S}^{{\em Inf\/},k,{\cal C}}$ or ${\cal C}_{TD} =  {\cal
S}^{{\em Inf\/}, k,{\cal C}}_{{\em neg}}$ and to augment the input of the bottom-up prover by this set 
(see Section \ref{sgclauses}).
Thus, we use again a filter function $\varphi_{TD}$ for selecting some subgoal clauses. That is, 
${\cal C}_{TD} = \varphi_{TD}({\cal S}^{{\em Inf\/},k,{\cal C}}) \subseteq {\cal S}^{{\em Inf\/},k,{\cal C}}$ or 
${\cal C}_{TD} = \varphi_{TD}({\cal S}^{{\em Inf\/},
k,{\cal C}}_{{\em neg}}) \subseteq {\cal S}^{{\em Inf\/},k,{\cal C}}_{{\em neg}}$.

Finally, we want to explain how our method---preprocessing and augmentation of the input 
of the provers---is indeed
well-suited for overcoming the disadvantages of the provers.

We start with the top-down prover. Usually the clauses ${\cal C}_{BU}$ generated by a superposition prover
are quite general because specialized clauses are eliminated by subsumption or rewriting. It is
hence quite probable that they can often be used for closing open branches of tableaux enumerated by a top-down
prover {\em without instantiating the tableaux}. If such a kind of lemma matching \shortcite<e.g.,>{Iw97} is possible we are able to close branches without introducing new subgoals or 
reducing the possibility that the remaining subgoals are solvable. If subgoals which often
occur in tableaux can be solved, the lemmas are a good means for redundancy control. Moreover, 
since the search scheme
of a superposition prover differs from that of an ME prover it is to be expected that it can generate clauses
with few inferences that can close a branch which could only be closed by many inferences when using no
lemmas. Then proof lengths are drastically reduced. See Section \ref{lemmas} 
for a more detailed description of the use of lemmas.

The input of a superposition prover is augmented by subgoal clauses which are the result of a
transformation of an original goal clause into subgoals. Hence, the goal-orientation of a superposition
prover is increased if it uses such transformed goal clauses in its inferences. Since the ME
prover employs a different search scheme it can very quickly conduct certain steps that the
superposition prover cannot reconstruct because of its heuristic search. 
The search for a proof can then be reduced. 

% -------------------------------------------------------------------------------------------------
\section{Subgoal Clauses for Top-Down/Bottom-Up Integration}
\label{sgclauses}
In this section we examine the integration of subgoal clauses
into the input set of a superposition prover. At first we assume that all subgoal clauses generated within a
certain number of inferences are added to the input set and we give some results regarding proof length and
search reduction. After that, we explain the necessity of selecting only some subgoal clauses and introduce
two selection methods based on the theoretic discussion.

\subsection{Reduction of Proof Length and Search through Subgoal Clauses}
\label{redls}
The cooperation  method introduced in the preceding section  gives rise to the question of whether a {\em proof length
reduction\/} is possible, i.e.\ whether there are shorter superposition proofs 
of the inconsistency of
${\cal C}\cup {\cal S}^{{\em Inf\/},k,{\cal C}}$ or ${\cal C}\cup {\cal S}^{{\em Inf\/},k,{\cal C}}_{{\em neg}}$ than of the inconsistency of ${\cal C}$. (Note that we measure the length of a proof $P$ by counting the number of inference steps $|P|$
in it.) Since some inference steps are necessary for enumerating subgoal clauses we should try to find
out whether these inferences can be saved when using the clauses. 

This question is mainly of theoretical interest because in general bottom-up
provers do not enumerate minimal proofs. Moreover, bottom-up provers usually perform a lot of unnecessary
inferences. It is more important to analyze whether a
bottom-up  prover can benefit from the use of subgoal clauses in the form  of a {\em
proof search reduction}, i.e.,\ a reduction of the number of inferences the prover needs in order
to find a proof.  It is particularly interesting to identify the cases of maximal proof search reduction.

\subsubsection{Subgoal clause generation via $CTC$}
\vspace{-0.2cm}
Firstly, we examine the case where we employ calculus $CTC$, i.e.\ generate ${\cal S}^{{\em Inf\/},k,{\cal C}}$.
We assume further that no equality is involved in the problem, i.e.\ superposition corresponds to (ordered)
resolution.  

\begin{theorem}\ \label{lala}
\begin{enumerate}
\item Let ${\cal C}$ be a set of ground clauses not containing equality, let $\Box\not\in\cal C$, and let
$k>1$ be a natural number. Let $P_1$ and $P_2$  be minimal length
resolution refutation proofs for ${\cal C}$
and ${\cal C}\cup {\cal S}^{{\normalsize\em Inf},k,{\cal C}}$, respectively. Then, it holds:
$|P_1| > |P_2|$.
\item For each $k>1$ there is a set of (non-ground) clauses ${\cal C}_k$ not containing equality
($\Box\not\in {\cal C}_k$),
such that no minimal length resolution refutation proof for ${\cal C}_k\cup {\cal S}^{{\normalsize\em Inf},k,{\cal C}_k}$
is shorter than a minimal length resolution refutation proof for ${\cal C}_k$.
\end{enumerate}
\end{theorem}

%\vspace{-0.2cm}
\noindent {\em Proof:}
\begin{enumerate}
\item Note that no factorization steps are needed in the case of ground
clauses (recall that clauses are sets of literals). Then, the claim is trivial since the result
of the first resolution step of each minimal proof is an element of ${\cal S}^{{\em Inf\/},k,{\cal C}}$.
\item Let $k>1$. Let ${\cal C}_k$ be defined by ${\cal C}_k = \{\{\neg p(x_1),\ldots,
\neg p(x_k)\}, \{p(y_1),\ldots,p(y_k)\}\}$. Let $>=\emptyset$ be the ordering used for ordered resolution. Then,
a minimal resolution refutation proof for ${\cal C}_k$ requires
$k-1$ binary factorization steps (resulting in the clause $\{p(y_1)\}$) and $k$ resolution steps.
Furthermore, it can easily be recognized that there are in ${\cal S}^{{\em Inf\/},k,{\cal C}_k}$ only clauses which contain at least one positive and one
negative literal. Thus, none of these clauses can lead to a refutation proof for ${\cal C}_k\cup {\cal
S}^{{\em Inf\/},k,{\cal C}_k}$ in less than $2k-1$ inferences. $\hfill\Box$
\end{enumerate} 

Hence, a reduction of the proof length is at least possible in the ground case.
The (heuristic) proof search of a
resolution-based prover may not profit from the proof length reduction obtained. For example it is
possible that all clauses of a minimal refutation proof of $\cal C$ have smaller heuristic weights than the
clauses from ${\cal S}^{{\em Inf\/},k,{\cal C}}$ and will hence be activated before them. Consider following 
example:

\begin{example}\ {\em
Let $>=\emptyset$ be the ordering used for ordered resolution. Let the clause set ${\cal C}$ be given by ${\cal
C} = \{\{\neg a,\neg b,c\}, \{\neg g, b\}, \{a\}, \{g\}, \{\neg c\}\}$.
The heuristic ${\cal H}$ corresponds to the FIFO heuristic. Furthermore, for the first $n$ activation steps ($n \in \nat,\ n \geq 9$),
 resolvents of the two most recently activated clauses are preferred
by ${\cal H}$. Then, following clauses are activated by the prover (in this order): $\{\neg a,\neg b, c\}, 
\{\neg g, b\}, \{\neg a,\neg g, c\}, \{a\}, \{\neg g, c\}, \{g\}, \{c\}, \{\neg c\}, \Box$. Furthermore, if the subgoal clauses
of ${\cal S}^{{\em Inf\/},k,{\cal C}}$ are inserted behind the original axioms
the prover will find the same resolution refutation proof for ${\cal C}\cup {\cal S}^{{\em Inf\/},k,{\cal C}}$
($k\ge 0$) and the proof search does  not benefit from a possible proof length reduction.} 
\end{example}


Since the above example (especially the chosen heuristic) is somewhat contrived, it can be expected for many problems
 that clauses from ${\cal S}^{{\em Inf\/},k,{\cal C}}$ will be activated. In this 
case there is also no guarantee that the proof search is improved because the subgoal clauses can 
import additional redundancy.  

%An interesting sub-logic of full first-order logic is Horn logic. In this area, since often bottom-up
%provers then employ positive hyper-resolution \shortcite<e.g., \otter>{Mc94}, we can make the reduction of the
%proof length more precise.            

$CTC$ differs---apart from the lack of factorization---mainly in the handling of equality from the superposition
calculus.  In the case that equality is involved in the problem, a proof length reduction 
even for ground clauses is not guaranteed. 

\noindent
\begin{theorem}\ \label{theoNOnHornEQ} For each resource $k>1$ there is a set of ground
unit equations $\cal C$ ($\Box\not\in {\cal C}$) where the minimal superposition refutation proofs for
${\cal C}\cup {\cal S}^{{\normalsize\em Inf},k,{\cal C}}$ are not shorter than minimal proofs for $\cal C$.
\end{theorem}
\vspace{-0.2cm}
\noindent {\em Proof:} Let $>=\emptyset$ be the ordering used for superposition. Consider the set of unit
equations ${\cal C}=\{\{a=b\}, \{f^{k-1}(a)\neq f^{k-1}(b)\}\}$.
We assume that $>=\emptyset$ is used as an ordering for superposition.
Then, a minimal superposition refutation proof for ${\cal C}$ requires two inferences, a superposition
step into $f^{k-1}(a)\neq f^{k-1}(b)$ resulting in the inequation $f^{k-1}(a)\neq f^{k-1}(a)$, and then an
equality
resolution step. In the set ${\cal S}^{{\em Inf\/},k,{\cal C}}$ are either non-unit clauses whose refutation
requires at least 2 inferences or the units ${\cal U} = \{\{f^i(a)\neq f^i(b)\}, \{f^j(a)=f^j(b)\}: 0\le i< k-1, 0< j\le k-1\}$.
 Since the
refutation of ${\cal C}\cup {\cal U}$ also requires 2 inferences a reduction of the proof length is
impossible. $\hfill\Box$


%All in all, a reduction of the heuristic search for a proof cannot be
%guaranteed, although proof lengths---at least for ground clauses and if no equality is involved in the 
%problems---are reduced. This is the case if subgoal clauses are ignored by the superposition prover
%or if they import too much additional redundancy. 
In summary a reduction of the heuristic search for a proof cannot be guaranteed 
because the proof length may not be reducible, the subgoal clauses may be ignored by the 
superposition prover, or the subgoal clauses
may import too much additional redundancy. The two latter points also hold in the ground 
case without equality where at least a proof length reduction is guaranteed.

The second point is no real problem since---as our experiments
showed---usually subgoal clauses will be activated and will be involved in the search
process of a prover. The risk that subgoal clauses are ignored can  be minimized by
selecting especially such subgoal clauses which will take part in the search with a
high probability, e.g.\ clauses with a small heuristic weight regarding the heuristic
of a superposition prover. In our selection process we need not use such a focus
according to the experimental results.
The first and third point show some theoretical weaknesses but in connection with
appropriate relevancy-based selection techniques we could observe in practice
that a restructuring of the search caused by using subgoal clauses allows proofs to be found faster. 

\subsubsection{Subgoal clause generation via $CTC_{{\em neg}}$}
Secondly, we examine the case where we employ the calculus $CTC_{{\em neg}}$, i.e.\ generate ${\cal S}_{{\em neg}}^{{\em Inf\/},k,{\cal C}}$.
Then, even for ground clauses not containing equality it is possible that minimal proofs cannot be 
shortened when employing subgoal clauses.

\noindent
\begin{theorem}\ There is a set of ground clauses $\cal C$ where no minimal length resolution refutation
proof for ${\cal C}\cup {\cal S}_{\normalsize\em neg}^{{\normalsize\em Inf},2,{\cal C}}$ is shorter than
a minimal length resolution refutation proof for $\cal C$.
\end{theorem}
\vspace{-0.3cm}
\noindent {\em Proof:} Consider the following set $\cal C$ of clauses (again we employ $>=\emptyset$): 
\[{\cal C} = \left\{\begin{tabular}{ccc}
                       $\{l_4, l_6, l_7\}$, & $\{l_4, l_6, \neg l_7\}$, & $\{l_3, \neg l_4\}$, \\
                       $\{l_3, \neg l_6\}$, & $\{\neg l_2, \neg l_4\}$, & $\{l_4, \neg l_5, \neg l_6\}$, \\
                       $\{\neg l_2, l_5\}$, & $\{l_1, l_2, \neg l_3\}$, & $\{\neg l_1, l_2, \neg l_3\}$ \\
                   \end{tabular} \right\} \]
Each minimal refutation proof for this set requires 9 resolution steps,
e.g.:

\vspace{0.3cm}
\begin{tabular}{llll}
$[1, ax]$ & $\{l_4, l_6, l_7\}$ & $[10, res(1,2)]$ & $\{l_4, l_6\}$\\
$[2, ax]$ & $\{l_4, l_6, \neg l_7\}$ & $[11, res(6,10)]$ & $\{l_4, \neg l_5\}$\\
$[3, ax]$ & $\{l_3, \neg l_4\}$ & $[12, res(3,10)]$ & $\{l_3, l_6\}$\\     
$[4, ax]$ & $\{l_3, \neg l_6\}$ & $[13, res(7,11)]$ & $\{\neg l_2, l_4\}$\\      
$[5, ax]$ & $\{\neg l_2, \neg l_4\}$ & $[14, res(5,13)]$ & $\{\neg l_2\}$\\
$[6, ax]$ & $\{l_4, \neg l_5, \neg l_6\}$ & $[15, res(4,12)]$ & $\{l_3\}$\\
$[7, ax]$ & $\{\neg l_2, l_5\}$ & $[16, res(8,9)]$ & $\{l_2, \neg l_3\}$\\         
$[8, ax]$ & $\{l_1, l_2, \neg l_3\}$ & $[17, res(14,16)]$ & $\{\neg l_3\}$\\
$[9, ax]$ & $\{\neg l_1, l_2, \neg l_3\}$ & $[18, res(15,17)]$ & $\Box$\\
\end{tabular}
\vspace{0.3cm}

Now, it holds: 

\[{\cal S}_{{\em neg}}^{{\em Inf\/},2,{\cal C}} = \left\{ \begin{tabular}{ccc}
                               $\{\neg l_2, l_6, l_7\}$, & $\{\neg l_2, l_6, \neg l_7\}$, & $\{l_1,
\neg l_3, \neg l_4\}$, \\
                               $\{\neg l_1, \neg l_3, \neg l_4\}$, & $\{\neg l_2, \neg l_5, \neg l_6\}$ \\
                       \end{tabular} \right\} \]

When enumerating all proofs for ${\cal C}\cup {\cal S}_{{\em neg}}^{{\em Inf\/},2,{\cal C}}$ one can recognize that
the minimal proof length cannot be reduced. $\hfill\Box$

%Note that the above example contains non-Horn clauses. Many interesting problems,
%however, can be specified in Horn logic. Thus, it is interesting to investigate whether or not a proof 
%length reduction is possible in the case that only Horn problems are considered. 
%Since often in this area bottom-up provers employ positive hyper-resolution 
%\shortcite<e.g., \otter,>{Mc94}, we assume that we have a bottom-up prover also employing this resolution variant.
%Then, it is not only always possible to reduce the proof length but we can even make the reduction of
%the proof length more precise. 
%
%In order to do this, we employ following notions:
%For natural numbers $a$ and $b$, $a\monus b$ is equal to $a-b$ if $a>b$, otherwise it is equal to 0. $\frac{a}{b}$
%denotes the maximal number $z$ such that $z\cdot b < a$. Moreover, for a set of clauses $\cal C$,
%$max_{{\em neg}}({\cal C})$ is the maximal number of negative literals which occur in a clause from $\cal C$.
%
%\begin{theorem}\ Let ${\cal C}$ be a set of Horn clauses, $\Box\not\in\cal C$. If $P_1$ and $P_2$ are
%minimal positive hyper-resolution proofs for ${\cal C}$ and ${\cal C}\cup {\cal S}_{neg}^{Inf,k,{\cal C}}$,
%respectively, then  \[|P_1|\monus k\le |P_2| \le |P_1|\monus \frac{k}{max_{neg}({\cal C})}\]
%\end{theorem}
%\vspace{-0.3cm}
%\noindent {\em Proof:} Let $Neg({\cal C})=\{\neg g_1^1\vee \ldots\vee
%\neg g_{n_1}^1, \ldots, \neg g_1^m\vee \ldots\vee\neg g_{n_m}^m\}$, where each $\neg g_1^i\vee
%\ldots\vee\neg
%g_{n_i}^i$ ($1\le i\le m$) is part of a minimal positive hyper-resolution refutation proof for ${\cal C}$.
%Note that in each minimal hyper-resolution proof exactly one negative clause occurs since the result of a
%hyper-resolution step involving a negative clause is the empty clause.\\
%Firstly, we show that there are clause sets ${\cal C}_k$ where the minimal proof length $|P_2|$
%when employing subgoal
%clauses is equal to $|P_1|\monus k$. Such clause sets must be construed in such a way that each
%resolution step applied to a subgoal clause entails that one hyper-resolution step is saved.
%We define ${\cal C}_k$ by ${\cal C}_k = \{\{\neg g\}, \{\neg
%a_1, g\},$ $\{\neg a_2, a_1\},\ldots, \{\neg a_k, a_{k-1}\}, \{a_k\}\}$. Then, obviously the proof length
%can be reduced to the value $|P_1|\monus k$.\\
%Secondly, we show that for each $k$ there are clause sets ${\cal C}_k$ where the minimal proof length $|P_2|$
%when
%employing subgoal
%clauses is equal to $|P_1|\monus \frac{k}{max_{neg}({\cal C}_k)}$. In order to do this we must construct
%clause sets ${\cal C}_k$ where $max_{neg}$ resolution steps are necessary in order to save one
%hyper-resolution step. We define the clause set ${\cal C}_k$ by ${\cal C}_k =
%\{\{\neg g_1, \ldots, \neg g_k\}, \{g_1\}, \ldots,\{g_k\}\}$. Then, obviously the proof length
%can be reduced to the value $|P_1|\monus \frac{k}{max_{neg}({\cal C})}$.\\
%Finally, we have to show that for each clause set $\cal C$ the minimal proof length when employing subgoal clauses
%is within the claimed limits. We perform induction over $k$:\\\vspace{0cm}
%
%$k=1$: We distinguish between two cases: On the one hand it might be that all subgoals of clauses in $Neg({\cal C})$ 
%can be closed with axioms immediately. Then, if $k\ge minL(Neg({\cal C})) = \min(\{|C|:C\in Neg({\cal C})\})$ then $\Box \in {\cal
%S}_{neg}^{Inf,k,{\cal C}}$. Hence, $|P_2| = 0$, i.e.\ $0=|P_1|\monus k\le |P_2|\le |P_1|\monus
%\frac{k}{max_{neg}({\cal C})}\in\{0,1\}$. If $k<minL(Neg({\cal C}))$, then for all minimal proofs $P_2$ it holds
%$|P_2| = |P_1| = 1$, i.e.\ $0=|P_1|\monus k\le |P_2|\le |P_1|\monus \frac{k}{max_{neg}({\cal C})} = 1$.
%On the other hand, it might be that there is a subgoal of a clause from $Neg({\cal C})$ that cannot be solved with
%an axiom immediately. Then, in ${\cal S}_{neg}^{Inf,k,{\cal C}}$ there is a subgoal clause
%$\neg g_1^i\vee\ldots\vee \neg g_{u-1}^i\vee\neg\sigma(a_1^i)\vee\ldots\vee
%\neg\sigma(a_{z_i}^i)\vee\neg g_{u+1}^i\vee\ldots\vee \neg g_{n_i}^i$ for some $i$ ($1\le
% i\le
%m$), if there is a rule $a_1^i\wedge\ldots\wedge a_{z_i}^i\to {g_u^i}^\prime$ ($1\le u\le n_i, \sigma =
%mgu({g_u^i}^\prime, g_u^i$)) in $\cal C$ and a minimal refutation proof uses this rule.
%Then, $|P_2| = |P_1| - 1$ because the 
%hyper-resolution step involving $a_1^i\wedge\ldots\wedge a_{z_i}^i\to {g_u^i}^\prime$ in
% order to generate an instance of ${g_u^i}^\prime$ is saved. Hence, $|P_1|\monus k\le |P_2| \le
%|P_1|\monus \frac{k}{max_{neg}({\cal C})}\in \{|P_1|-1, |P_1|\}$.\\\vspace{0cm}
%
%$k\to k+1$: When applying the induction hypotheses we obtain: There is a subgoal clause $C^k\in {\cal
%S}_{neg}^{Inf,k,{\cal C}}$ such that for each minimal hyper-resolution proof (of the inconsistency of
%${\cal C}\cup {\cal S}_{neg}^{Inf,k,{\cal C}}$) $P_2^k$ 
%which employs this clause holds: $|P_1|\monus k\le |P_2^k| \le |P_1|\monus \frac{k}{max_{neg}({\cal C})}$.\\
%If $C^k = \Box$ then $|P_2^k| = 0$ and also for all minimal proofs $P_2^{k+1}$ of the inconsistency
%of ${\cal C}\cup {\cal S}_{neg}^{Inf,{k+1},{\cal C}}$ we have $|P_2^{k+1}| = 0$. Thus, $|P_2^{k+1}|$ is 
%in the claimed range. \\
%In the following we can hence assume that $C^k \neq \Box$.
%At first we assume that a minimal proof $P_2^{k+1}$ of the inconsistency of ${\cal C}\cup {\cal S}_{neg}^{Inf,{k+1},{\cal C}}$
%uses a clause which can be derived from such a clause $C^k$ with one resolution step.
%We again distinguish between two cases: \\
%On the one hand it might be that all subgoals of this clause $C^k$ can be
%solved with axioms immediately. Then: If a subgoal $sg\in C^k$ can be closed that has no brother, i.e.\ no
%other subgoals introduced by the extension that lead to $sg$ are in $C^k$, we obtain by closing $sg$ with
%an axiom the clause $C^{k+1}$ being an element of ${\cal S}_{neg}^{Inf,{k+1},{\cal C}}$. $C^{k+1}$ allows
%for a minimal superposition proof $P_2^{k+1}$ which needs only $|P_2^k|-1$ inferences. Since $|P_1|\monus
%k\le |P_2^k|$, also $|P_1|\monus (k+1)\le |P_2^{k+1}|$. Moreover, since $|P_2^k| \le |P_1|\monus
%\frac{k}{max_{neg}({\cal C})}$, also $|P_2^{k+1}| = |P_2^k|-1 \le |P_1|\monus \frac{k+1}{max_{neg}({\cal
%C})}$. Otherwise, if all subgoals of $C^k$ have brothers, for all minimal proofs $P_2^{k+1}$ we have
%$|P_2^{k+1}| = |P_2^k|$. Then, obviously $|P_1|\monus (k+1)\le |P_2^{k+1}|$. When considering the upper
%bound we obtain: If $|P_2^k|<|P_1|\monus \frac{k}{max_{neg}({\cal C})}$, then $|P_2^{k+1}| = |P_2^k|\le
%|P_1|\monus \frac{k+1}{max_{neg}({\cal C})}$. If $|P_2^k| = |P_1|\monus \frac{k}{max_{neg}({\cal C})}$ and
%$max_{neg}\not{\hspace{-0.1cm}|} (k+1)$, $|P_2^{k+1}| = |P_2^k| = |P_1|\monus \frac{k+1}{max_{neg}({\cal C})}$. $|P_2^k| =
%|P_1|\monus \frac{k}{max_{neg}({\cal C})}$ and $max_{neg}|(k+1)$ is impossible because in this case in $C^k$
%there must
%be a subgoal having no brother.\\
%%
%%
%% ohne Beweis ist intuitiv klar
%%
%%
%On the other hand, there might be a subgoal in $C^k$ that can be extended. Such an extension leads to a
%clause $C^{k+1}\in {\cal S}_{neg}^{Inf,{k+1},{\cal C}}$ that is part of a minimal proof $P_2^{k+1}$ with
%$|P_2^{k+1}| = |P_2^k|-1$. Then, since $|P_1|\monus k\le |P_2^k|$, also $|P_1|\monus (k+1)\le
%|P_2^{k+1}|$. Moreover, since $|P_2^k| \le |P_1|\monus
%\frac{k}{max_{neg}({\cal C})}$, also $|P_2^{k+1}| = |P_2^k|-1 \le |P_1|\monus \frac{k+1}{max_{neg}({\cal
%C})}$. \\
%Now, we assume that a minimal proof $P_2^{k+1}$ uses a subgoal clause which is not derived from
%a clause $C^k$. Then, no proof involving a subgoal clause derived from a clause $C^k$ has a proof length
%smaller than $|P_2^k|$. 
%Hence, we know
%that $|P_2^{k+1}| = |P_2^k|$ (because one resolution step can only save one hyper-resolution step).
%Moreover, we know that all subgoals of clauses $C^k$ can be closed with axioms immediately and that all these
%subgoals have brothers (otherwise minimal proofs must only contain subgoal clauses derived with one resolution step 
%from a $C^k$). By using the same arguments as above we can see that $|P_2^{k+1}|$ is within the claimed limits.
% $\quad\Box$
%
%Nevertheless, in analogy to before also in this context the proof search need not profit from the proof 
%length reduction obtained.
% But our experiments have shown that often also proof search reductions are possible.

In the case where equality is involved in our proof problems, we obtain a theorem 
analogous to the previous one:

\noindent
\begin{theorem}\ For each resource $k>1$ there is a set of unit equations $\cal C$ where the minimal
superposition refutation proofs for
${\cal C}\cup {\cal S}_{\normalsize\em neg}^{{\normalsize\em Inf},k,{\cal C}}$ are not shorter than minimal proofs for $\cal C$.
\end{theorem}
\vspace{-0.2cm}
\noindent {\em Proof:} In analogy to Theorem \ref{theoNOnHornEQ}. $\hfill\Box$                      

% kommt weg falls kpomplexerer Satz hin kommt
We can recognize that for $CTC_{{\em neg}}$ the results are essentially the same as for $CTC$.
In general the reduction of the heuristic search for a proof cannot be
guaranteed and proof lengths may not always be reduced.
In practice, however, we could again observe that a restructuring of the search caused
by subgoal clauses often allows proofs to be found faster. 

In the following we simply assume that
inferences with subgoal clauses are not omitted by a superposition prover, i.e.\ that they are
involved in the proof search. We want to deal
in more detail with the problem of identifying subgoal clauses which can lead to a large reduction of the search effort and
how we can efficiently select such subgoal clauses. This problem has to be tackled with
heuristics since there is---as we have examined---no theoretical guarantee and also
no method to decide whether subgoal clauses are useful.

\subsection{Relevancy-Based Generation of Subgoal Clauses}
Even when using small resources $k$ the sets ${\cal S}^{{\em Inf\/},k,{\cal C}}$ and ${\cal S}^{{\em Inf\/},k,{\cal
C}}_{{\em neg}}$ can become quite large. Thus, it is
not sensible to integrate all subgoal clauses from ${\cal S}^{{\em Inf\/},k,{\cal C}}$ or ${\cal S}^{{\em Inf\/},k,{\cal
C}}_{{\em neg}}$ into the search state of a
superposition-based prover. Integrating too many clauses usually does not entail a favorable rearrangement
of the search because the heuristic ``gets lost'' in the huge number of clauses which can be derived from 
many subgoal clauses. It is hence reasonable to develop techniques for filtering subgoal clauses 
that appear to
entail a large gain in efficiency for a superposition prover if they can be
proven. That is, we are interested in filtering {\em relevant\/} subgoal clauses. As already described in
Section \ref{framework},
we generate a {\em set of subgoal clause candidates\/} and then we select some subgoal clauses
from this set. The chosen subgoal clauses are added to the search state of the bottom-up prover. 
In the following, we will at first introduce some criteria for measuring the relevancy of a
clause. Then, we shall introduce two techniques for generating subgoal clause candidates and        
deal with the selection of relevant subgoal clauses.

\subsubsection{Relevancy Criteria for Subgoal Clauses}
Two main characteristics of subgoal clauses can contribute to a speed-up of the proof search.

Firstly, since according to Section \ref{redls} subgoal clauses introduce additional redundancy it
is important that some of the clauses can be proven quite easily, that is more easily than
the original goal(s). In order to estimate this, it is necessary to judge whether they can {\em probably be
solved\/} with the help of clauses of the input set. Measuring similarity between a goal
and other clauses with the techniques developed by \shortciteA{DF94}, \shortciteA{DFF97}, or \shortciteA{FuM97c} may be well-suited for this estimation.

Secondly, a solution of a newly introduced subgoal clause {\em should not always entail a solution of an original
goal within
few steps of the superposition-based prover}. If this were the case then the integration of new subgoal clauses would not promise
much
gain.  Criteria in order to estimate this are: Firstly, the transformation of an original goal
clause into a subgoal clause by an ME prover should have been performed by using many inferences, i.e.\ $k$
should
be quite high. Then, a solution of a new subgoal clause usually does not entail a solution of an
original goal within few steps because the probability is rather high that a bottom-up prover
cannot---due to its heuristic search---quickly reconstruct the inferences needed to infer the original goal.
Secondly, if there is a subgoal clause $S_T$ and some of the tableau clauses of the tableau $T$
have a
high heuristic weight w.r.t.\ the heuristic of the superposition-based prover, a high gain of efficiency
can be expected if the prover can prove $S_T$. This is due to the fact that inferences needed to infer the
original goal using $S_T$ are difficult for the superposition-based prover.

\subsubsection{Efficient Generation and Selection of Subgoal Clauses}
In order to generate a set of interesting subgoal clauses it is important that we employ a large resource
for generating subgoal clauses. As we have already discussed, subgoal clauses that are generated with a small
number of inferences do not promise much gain because a bottom-up prover may easily reconstruct the
inferences needed to infer them. However, it is not possible
to generate all subgoal clauses ${\cal S}^{{\em Inf\/},k,{\cal C}}$ or ${\cal S}^{{\em Inf\/},k,{\cal C}}_{{\em neg}}$ for a sufficiently large resource $k$ as subgoal clause
candidates because their huge number means that the costs of generation and additional
selection are too high. Hence, we must restrict ourselves to a set of subgoal clause candidates that is 
a {\em subset\/} of ${\cal S}^{{\em Inf\/},k,{\cal
C}}$ or ${\cal S}^{{\em Inf\/},k,{\cal C}}_{{\em neg}}$, $k$ sufficiently large (see Section \ref{experimente}).


\begin{figure*}
\hspace{1.0cm}
 \epsfxsize120mm
\epsfbox{dseinerstes.eps}
\caption{\label{fig::infbased}Inference-based generation of a set of subgoal clause candidates}
\end{figure*}

Our first variant, an {\em inference-based\/} method, starts by generating subgoal clauses from
${\cal S}^{{\em Inf\/},k,{\cal C}}$ or ${\cal S}^{{\em Inf\/},k,{\cal C}}_{{\em neg}}$ for a rather large resource $k$ and stops when $N_{sg}$ subgoal clause candidates are generated. 
The advantage of this method is that it is very easy and can be
efficiently implemented. Tableaux are enumerated with a fixed strategy for selecting subgoals for inferences (usually
left-most/depth-first) and for each tableau its subgoal clause is stored. The main disadvantage of this
method is that due to the fixed strategy and the limit of the number of subgoal clauses, we only obtain
subgoal clauses which are inferred from goal clauses by expanding particular subgoals with a large
number of inferences and other subgoals with only a small number of inferences. (See also Figure \ref{fig::infbased}: Ovals are
tableaux in a finite segment of the search tree ${\cal T}$, the lines represent the $\vdash$ relation.
Grey ovals represent enumerated tableaux, i.e.\ their subgoal clauses are stored, white ovals represent tableaux which are not enumerated.) Thus, the method is
somewhat unintelligent because no information about the quality of the transformation of an original goal
clause into a subgoal clause is used. Certain transformations are favored against others only due to the
uninformed subgoal selection strategy.

Our second variant, an {\em adaptive\/} method, tries to overcome these disadvantages in the following
way: Instead of permitting more inferences when generating subgoal clauses due to an uninformed subgoal
selection strategy, we want to allow more inferences at certain {\em interesting positions\/} of the search
tree ${\cal T}$ for a given set of clauses $\cal C$. 

In detail, our approach is as follows: 
At first, we generate all subgoal clauses ${\cal S}^{{\em Inf\/},k_1,{\cal C}}$ or ${\cal S}^{{\em Inf\/},k_1,{\cal C}}_{{\em neg}}$ 
with a resource $k_1$ which is smaller compared to the first variant.
Then, a fixed number $N_{{\em ref}}$ of subgoal clauses is chosen which
promise the highest gain of efficiency regarding the previously mentioned criteria. More exactly, we choose subgoal clauses
which are maximal w.r.t.\ a selection function $\psi$. One possible           
realization of $\psi$ is:

\vspace{-0.2cm}
\[\psi(S_T) = \alpha_1\cdot I(S_T) + \alpha_2\cdot\max(\{{\cal H}(C):C\mbox{ is a tableau
clause in } T\})\]
\vspace{-0.8cm}
\[\hspace*{2.3cm} + \hspace{0.1cm} \alpha_3\cdot\max(\{sim(S_T,C): C\in {\cal C}, |C| = 1\})\]
\vspace{-0.3cm}

The higher the number of inferences $I(S_T)$ which are needed to infer $S_T$, the higher 
$\psi(S_T)$ should be. Hence, $\alpha_1$ should be positive. Setting $\alpha_2>0$ is also
sensible. If there are tableau
clauses in $T$ which have a high heuristic weight regarding the heuristic ${\cal H}$ of the
superposition-based prover we can---as already discussed---gain a lot of efficiency. The function $sim$ measures whether literals
from $S_T$ can probably be solved with unit clauses from $\cal C$. It maps a pair of clauses to a real number.
The larger $sim(S_T,C)$ the larger the similarity between $S_T$ and the unit clause $C$. We utilize a variant of
the function $occnest$
which is defined by \shortciteA{DF94} for accomplishing the task. We set $\alpha_1>\alpha_2>\alpha_3\ge 0$ due to the increasing vagueness of
the criteria.


\begin{figure*}
\hspace{0.8cm}
 \epsfxsize130mm
\epsfbox{dseinzweites.eps}
\caption{\label{fig::adaptive}Adaptive generation of a set of subgoal clause candidates}
\end{figure*}

Now, let $M^{N_{{\em ref}}}\subseteq {\cal S}^{{\em Inf\/},k_1,{\cal C}}$ or $M^{N_{{\em ref}}}\subseteq {\cal
S}^{{\em Inf\/},k_1,{\cal C}}_{{\em neg}}$ be the set of chosen subgoal clauses. Then, we generate
subgoal clauses with a resource $k_2$ but employ the clauses from  $M^{N_{{\em ref}}}$ as start clauses 
for the subgoal clause
enumeration. 
We call the set of subgoal clauses generated with this
method ${\cal S}^{{\em Inf\/},k_2, {\cal C}, M^{N_{{\em ref}}}}$. 
(Consider also Figure \ref{fig::adaptive}: The dotted line shows which
subgoal clauses are generated with resource $k_1$. Then some of them are selected (black ovals) and used as starting
points for the generation of new subgoal clauses with resource $k_2$.) The resource $k_2$ should again not be too high in order to
allow a fast enumeration of the subgoal clauses. The set of subgoal clause candidates is then given by ${\cal S}^{{\em Inf\/},k_1,{\cal
C}}\cup {\cal S}^{{\em Inf\/},k_2, {\cal C}, M^{N_{{\em ref}}}}$ (if we employ $CTC$) or by ${\cal S}^{{\em Inf\/},k_1,{\cal
C}}_{{\em neg}} \cup {\cal S}^{{\em Inf\/},k_2, {\cal C}, M^{N_{{\em ref}}}}$ (if we employ $CTC_{{\em neg}}$). Thus, subgoal clause candidates are on the one
hand all subgoal clauses derived with a certain number $k_1$ of inferences such that
it can be assumed that the proof length is reduced.
On the other hand, we have some subgoal clause candidates 
which are derived with a higher number of inferences, at most $k_1+k_2$. These subgoal clauses promise
a high gain of efficiency because they are derived from subgoal clauses selected with function $\psi$. That
is, they are derived from clauses which are considered to be very relevant for a superposition-based theorem prover.

For selecting subgoal clauses from the set of subgoal clause candidates we employ function $\varphi$---which is
mainly based on the function $\psi$---and select clauses with the highest weight regarding $\varphi$. $\varphi$ is defined by

\[\varphi(S_T) = \psi(S_T) - \theta(S_T).\]

 $\theta$ simply counts a
weighted sum of the number of variables in $S_T$ and two times the number of function or predicate symbols in
$S_T$. Hence, quite ``general'' subgoal clauses are preferred. This is sensible 
because they can usually be solved more easily.                             


% -------------------------------------------------------------------------------------------------
\section{The Use of Lemmas in Model Elimination}
\label{lemmas}
In this section we examine theoretical and practical aspects concerning the integration of superposition-generated lemmas          
into the input set of a model elimination prover. 
%At first we discuss general aspects regarding the advantages and disadvantages of lemma use in
%ME. We specifically deal with the relationship of the problem to find relevant lemmas and the
%{\em utility problem\/} \shortcite<see>{Min90} from the area of explanation-based learning and macro operator learning.
At first, we present some results regarding proof length and search reductions. 
As before, we measure the proof length by the number of inferences in it. Proof search is measured 
by the number of inferences the prover must perform in order to find a proof.
Then, we introduce some methods for a relevancy-based filtering of lemmas.


\subsection{Proof Length Reduction}
\label{lemmaprooflength}
When adding positive unit lemmas ${\cal C}_{BU}$ of a bottom-up prover to the axiomatization
${\cal C}$ of a top-down prover, a proof length reduction is possible if the following situation
occurs. If $T$ is a tableau that represents a proof and $sg$ is
a literal which has a depth smaller than $n-1$ of a branch in $T$ with depth $n$ we can
reduce the proof length if $\ng sg$ is unifiable with a lemma $l\in {\cal C}_{BU}$. Hence, we
are interested in the question of whether we can find lemmas useful in the described sense if we
choose ${\cal C}_{BU} = \varphi_{BU}(\{C:C\mbox{ is a fact}, C\in {\cal F}^{A,i}\})$  as
proposed in Section \ref{framework}. Unfortunately, even if $\varphi_{BU}$ selects all facts in $\{C:C\mbox{
is a fact}, C\in {\cal F}^{A,i}\}$ and $i$ is arbitrary large there is no guarantee that we can
find a useful lemma in this set. This is even true if the bottom-up prover
employs a fair heuristic.

\begin{theorem}\ For each $i\in\nat$ there is a clause set ${\cal C}_i$ and a fair heuristic
${\cal H}_i$ such that no positive unit lemma from ${\cal F}^{A,i}$ (generated by a resolution prover starting with ${\cal C}_i$ and
employing heuristic ${\cal H}_i$) can reduce the proof length of a proof for ${\cal C}_i$ with
$CTC$ ($CTC_{\normalsize\em neg}$).
\end{theorem}
\vspace{-0.2cm}
\noindent {\em Proof:} Let $i$ be a natural number and $>=\emptyset$ be the ordering used for ordered resolution.
For a literal $l$, $|l|$ denotes the number of
symbols in $l$. Set ${\cal C}_i=\{\{p(a)\}, \{\neg p(x), p(f(x))\}, \{\neg q(a)\},$ $\{\neg q(b), q(a)\}, \{q(b)\}\}$. 
Let ${\cal H}_i(\{l_1, \ldots, l_n\}) = \sum_{j=1}^n {\cal H}_i^L(\tilde{l_j})$, with
$\tilde{l_j} = l_j$, if $l_j$ is positive, and $\tilde{l_j} = \ng l_j$, otherwise.
Moreover, 

\[ {\cal H}_i^L(l) = \left\{\begin{array}{c@{\quad}l}
|l| & , l\equiv p(t), t\mbox{ is a term}\\
2+i+|l| & ,l\equiv q(t), t\mbox{ is a term.}\\
\end{array} \right. \]

Then it holds: For a fixed parameter $i$, ${\cal H}_i$ is a fair heuristic. Moreover, there are
only ME proofs of the inconsistency of ${\cal C}_i$ which contain literals with
top-symbol $q$. ${\cal F}^{A,i}$ contains only literals with top-symbol $p$, though. Hence, it
is impossible that a lemma of ${\cal F}^{A,i}$ is applicable. $\hfill\Box$

From a theoretical point of view we have again the negative result that in general 
useful lemmas are not elements of ${\cal F}^{A,i}$. However, empirical studies (see Section \ref{experimente})
reveal that in the most cases useful lemmas are generated by a superposition prover. Hence, we
assume that useful lemmas are in ${\cal C}_{BU}$ and henceforth examine which lemmas---being
part of a proof---can lead to a high proof search reduction of an ME prover.


\subsection{Proof Search Reduction}
\label{proofsearchred}
The effects regarding the structure of the search space of a $CTC$ ($CTC_{\em neg}$) prover caused by the use
of lemmas are closely related to the {\em utility problem\/} \shortcite<e.g.,>{Min90} from the area of explanation-based learning (EBL) and macro operator learning \shortcite<see also>{MS93}.
At the first sight, lemma use could be interpreted as
introducing new edges into the original search tree $\cal T$
because  a sub-deduction (proof of a lemma) can be reduced to one inference by
applying a lemma.
This corresponds to macro
operator learning or EBL where inference chains are
generalized and disjunctively stored as new operators or concept descriptions 
\shortcite<e.g.,>{Min90}, respectively.
We should notice, however, that
the use of lemmas
does not only insert new edges but
also 
new {\em nodes} into the search tree. This comes from the fact that the structure of a tableau $T_1$ where a 
lemma is applied
differs from the structure of an in other parts equal tableau $T_2$ where the lemma proof
is ``expanded''.
This has no influence on the inferences possible with $T_1$ and $T_2$
(the edges outgoing from the nodes $v_1$ and $v_2$ that are labeled with $T_1$ and $T_2$,
respectively)
but it has an effect on the value a completeness bound $\cal B$ assigns to the
tableaux. 
Considering the bounds introduced in Section \ref{framework},
$T_1$ can be enumerated with a resource value which is
smaller than or equal to that needed to enumerate $T_2$.
In analogy to macro operator learning and
considering these remarks,
we now summarize the advantages and disadvantages of using lemmas {\em in
connection with iterative deepening procedures}.

A minor advantage of introducing a lemma is the advantage of {\em
decreasing path costs}, i.e.\ the costs of reproducing the inferences needed
for its proof.  The major advantage of using lemmas is that they make a {\em restructuring of the
the search space possible\/}.

On the one hand, one can save the possibly high search effort needed for
proving a useful lemma (assuming the lemma proof can be expanded within the finite segment
 of
${\cal T}$ to be considered). 
On the other hand, it is possible that
a closed tableau can be reached within a smaller resource
value (``resource reduction'').  Then, the reordering effects usually allow us to solve problems
that
were previously out of reach because the search procedure gets lost in the
(usually exponentially) larger segment of the search tree defined by a larger resource.
It is clear, however, that this advantage only holds if the segment of the search tree
defined by the lower resource value is not increased too much by the use of the lemmas.
Considering our search bounds we can see that normally resource reductions
cannot be guaranteed when using superposition generated lemmas in an ME prover.
When using the inference bound a resource reduction is guaranteed
if by using lemmas a proof length reduction can be obtained. In the case
of the depth and weighted-depth bound in general not even a proof length 
reduction leads to a resource reduction.

Besides the positive effects of using lemmas, some negative effects
also occur. These stem from an increased redundancy.
The main disadvantage regarding the use of lemmas is the increase of the branching
rate of the search tree.
It is possible that a {\em misleading solution\/} of a subgoal may be obtained that could
not be found before within a given finite segment.
Even if a resource reduction from $n$ to $n^\prime < n$ occurs it is possible 
that solutions of
subgoals that could not be found with resource $n$ (without lemmas) can 
now be found with resource $n^\prime$ and lemmas. This can reorder the search
space in a hardly controllable manner. Considering the inference bound
in some cases tableaux which could not be enumerated with resource
$n$ can now be enumerated with lemmas.
It is possible that the use of lemmas ``spares'' more than $n-n^\prime$ inferences. 
If we use the depth bound it might be that in a tableau some
branches which can be closed in a depth greater than $n$ without
lemmas can now be closed in a depth smaller than or equal to $n^\prime$.
Then a lot of superfluous inferences can be introduced to the new minimal proof
segment. Analogous effects take place when using the weighted-depth bound
(especially also when using the configuration of the bound as described
by \shortciteA{MI97}).

Additionally, {\em duplications of segments of the search space}
can occur.  Assuming the expanded lemma proof lies
within the initial segment of $\cal T$ to be considered,
the use of an irrelevant lemma can cause a repeated exploration of
parts of the search space which does not contain a proof:
Since a superfluous
solution of a subgoal is found twice (via the lemma and by performing the inferences needed
to prove the lemma) the resulting superfluous inferences have to be performed
twice, too.
This disadvantage, however, can usually be overcome
by using local failure caching \shortcite{LMG94b}.

Besides these effects, which cause a restructuring of the search space,
it is even possible that the use of lemmas {\em increases the number of solutions}
of certain subgoals that exists in the whole search tree. This is because the use of lemmas 
can shadow well-known pruning
techniques like regularity since no regularity checks are possible in the proof
of a lemma.
Furthermore, the newly introduced lemmas cause the problem that in each inference
a possibly large number of lemmas has to be tested in order to determine whether
inferences are possible ({\em applicability test}). This necessitates new unification attempts.

In summation
our lemma mechanism is in general not able to produce lemmas that lead to a
proof length reduction and thus to a resource reduction.
Nevertheless experience shows that in many cases reductions of the proof length and the needed resource can
be obtained. 
When a small number of lemmas is sufficient for a resource reduction
the number of inferences which can be spared
by using lemmas can exceed the number of new superfluous inferences by magnitudes.
Thus, mechanisms are needed in order to select {\em relevant\/} lemmas from $\{C:C\mbox{ is a fact}, C\in {\cal
F}^{A,i}\}$ that should be inserted into ${\cal C}_{BU}$.
If we can find a rather small lemma set
which permits a resource reduction then in almost all cases 
we can find a proof much faster than would be possible without using lemmas (see
Section \ref{experimente}).
Note that the case of a large reduction of the proof length without a
reduction of the resource needed normally performs significantly worse than
the case of a small proof length reduction with a reduction of the resource needed.



\subsection{Relevancy-Based Lemma Selection}
Analogous to the foregoing section we now want to introduce some abstract
principles for filtering lemmas based on the discussion regarding the
structure of the search space. Then, we deal with concrete heuristics
applied for selecting lemmas.


\subsubsection{Relevancy Criteria for Lemmas}
%Finally, we want to discuss the cases where we can expect that using lemmas leads to such
%important resource reductions. If lemmas are able to solve arbitrary subgoals of a proof
%whose (sub-)proofs necessitate a large number of inferences
%especially inference oriented bounds can profit from this in form of a large resource
%reduction. 
%If some lemmas are able to solve subgoals that occur in a single deep branch of a proof
%especially depth-oriented bounds can profit because then a proof can be found in a smaller depth.
%
Since superposition provers employ a different search scheme than ME provers and since they
have effective mechanisms for handling equality, we can assume that a few subgoals which
are hard to solve (the proof necessitates a large resource w.r.t.\ a given completeness
bound) with an ME prover 
can be solved with lemmas. 
However, when using lemmas in order to close some subgoals of  an open tableau
the remaining open subgoals should be easy to solve w.r.t.\ the given bound.
Otherwise, we still cannot solve the problem within
a smaller resource. Note that we usually cannot expect 
that all branches of a proof can be ``shortened'' by superposition-generated 
lemmas. 
Since our lemma generation provides no guarantee that useful lemmas are generated 
(see Section \ref{lemmaprooflength}) usually only a small number of lemmas can be employed in a proof. 
All in all we obtain that
``interesting'' proofs (i.e.\ those we want to find) for an application of lemmas are 
proofs that contain many subgoals that are easy to solve---and can hence
be solved ``conventionally'' within a small resource---and only a few hard subgoals that must
be solved with lemmas. Then, we can expect that using lemmas leads to 
resource reductions.
Our filter techniques should hence try to find lemmas that
might be part of such proofs.

Furthermore, we should estimate how many new superfluous inferences
are introduced by a lemma. The integration
of new lemmas must not increase the branching rate too much. Otherwise, the gain of a possible
resource reduction is negated by the large overhead (see Section \ref{proofsearchred}).

These criteria lead us to three different filter functions that concentrate on certain aspects of
relevancy. The filter functions are well-suited for all of the previously
introduced completeness bounds.
Due to the vagueness of the filter criteria we use each filter function in order to choose
some lemmas (see Section \ref{experimente}). Note that it is better to select a few unnecessary lemmas
than to omit the selection of important ones.

\subsubsection{Expansion/Contraction-Based Selection}
The first filter function is called $\varphi_{BU}^S$. This function is rather simple and aims at
finding lemmas that do not lead to a high increase of the branching rate. 
$\varphi_{BU}^S$
accomplishes this by using knowledge obtained in the lemma generation (preprocessing) phase of the
bottom-up prover. In detail, $\varphi_{BU}^S$ selects facts with the highest value regarding a
judgment function $\psi_{BU}^S$.

\begin{definition}[{\bf Judgment function $\psi_{BU}^S$}]\ \\
{\em For a positive unit $l$, generated in the preprocessing phase, let $\varepsilon(l)$ and $\kappa(l)$ be
the numbers of expansion and contraction inferences, respectively, that $l$ was involved in. Then
\[\psi_{BU}^S(l) = \kappa(l) - \varepsilon(l).\]$\vspace{-0.3cm}$}
\end{definition}

$\psi_{BU}^S$ counts the inferences that each lemma candidate was involved in and rates expanding
inferences negative, contracting inferences positive. If a fact $l$ was often involved in an expanding
inference like resolution or superposition, then $l$ or many subterms of it  are unifiable with (subterms of)
(maximal) literals of axioms or derived clauses. Hence, if $l$ is added to the axiomatization of the
top-down prover it can be expected that $l$ or certain descendants of it can very often take part in extension 
steps. Since this
leads to a high increase of the branching rate we rate this negative. Of course, we are interested in the
fact that a lemma can be applied by the ME prover. However, since lemmas of a superposition prover
are usually quite general most of them may be used for closing occurring subgoals. Our criterion
aims mainly at excluding lemmas that are applicable in too many cases and hence introduce too many
solutions of subgoals that do not lead to a refutation of the input clauses. In contrast to expanding
inferences we rate contraction inferences positively. Indeed, ME provers do not have contracting
inferences. But as shown by \shortciteA{LSBB92}, subsumption can partly be simulated by {\em
subsumption constraints}. Hence, clauses that are able to contract many other clauses can support
search pruning techniques.

\subsubsection{Derivation-Based Selection}
The second filter function $\varphi_{BU}^D$ tries to select facts that are able to close 
subgoals that are very hard to solve with a connection-tableau-based 
prover. In order to estimate this, we consider  the 
derivation history of a fact.
We employ this filter function only if equality is involved in a problem.

\begin{example} {\em Let $\{f(f(x)) = g(x)\}$ and $\{h(b) = f(b)\}$ be axioms. Then, the clause
$\{g(b) = f(h(b))\}$ can be derived by one superposition step. However, if
$\neg g(b) = f(h(b))$ is a subgoal of an ME proof, its proof is more complicated (see Figure \ref{prooflala}).

\begin{figure*}
\hspace{3.0cm}
 \epsfxsize90mm
\epsfbox{cpbildung2.eps}
\caption{\label{prooflala} Simulating a superposition step with ME}
\end{figure*}

In general, if the superposition step is performed at a position $p$ and $|p|$ denotes the depth of
the position (above $|p| = 1$), then at most $|p|+5$ inferences are needed in order to prove the result
of such a superposition step. The proof necessitates at most a depth of $|p|+3$.} 
\end{example}

This example shows that the simulation of the specific equational operations of a superposition prover
necessitates a high depth as well as inference resource in an ME prover. That is, lemmas derived by many superposition steps are
able to close subgoals that cannot be solved by an ME prover within small resources. Hence, if such
lemmas are applicable large resource reductions possibly occur for depth or inference
oriented bounds. The judgment function
$\psi_{BU}^D$ employs this criterion. Again, the filter function $\varphi_{BU}^D$ selects facts with
the highest value regarding this judgment function.

\begin{definition}[{\bf Judgment function $\psi_{BU}^D$}]\ \\
{\em For a positive unit $l$ generated in the preprocessing phase, let $\psi_{BU}^D(l)$ be defined by
\[\psi_{BU}^D(l) = \left\{\begin{array}{c@{\quad}l}
0 & ,l\mbox{ is an axiom}\\
\psi_{BU}^D(l_1) + \psi_{BU}^D(l_2) + 1 & ,l\mbox{ is derived by a superposition step with premises }\\
                              &  \hspace{0.2cm} l_1\mbox{ and } l_2\\
\sum_{i=1}^n \psi_{BU}^D(l_i) & ,l\mbox{ is derived by a non-superposition inference }\\
                              & \hspace{0.2cm} \mbox{involving the literals } l_1, \ldots, l_n\ (n\in\nat).\\
\end{array} \right. \]}
\end{definition}

%We do not consider the exact position of the inference steps due to efficiency reasons. Because
%the positions are usually small ($\le 3$) their influence would also be small.

 

\subsubsection{Complexity-Based Selection}
Our third filter function $\varphi_{BU}^C$ aims at selecting lemmas that are able to solve some hard subgoals of
ME subgoal clauses such that the resulting open subgoals can easily be solved. Hence, the judgment function
$\psi_{BU}^C$ used by $\varphi_{BU}^C$ 
considers the sets of subgoal clauses ${\cal S}^{{\cal B},n,{\cal C}}$ or ${\cal S}^{{\cal B},n,{\cal C}}_{{\em neg}}$ for a certain resource $n$.
For each subgoal clause $sg$, if a lemma $l$ with $\psi_{BU}^{C, sg}(l) > 0$ exists,
the lemma $l$ with the highest judgment $\psi_{BU}^{C, sg}(l)$ is
selected  until a maximal number of lemmas is selected (see Section
\ref{experimente}).
This judgment is computed as follows. 


\begin{definition}[{\bf Judgment function $\psi_{BU}^{C, sg}$}]\ \\
{\em For a positive unit $l$ generated in the preprocessing phase and a subgoal clause $sg = \{l_1,\ldots,l_m\}$, let
$\psi_{BU}^{C, sg}(l)$ be defined in the following manner:\\
If no subgoal can be solved with $l$, i.e.\ $\neg\exists i, 1\le i\le m, \sigma:\sigma= mgu(\ng l_i, l)$,  then $\psi_{BU}^{C, sg}(l)=0$. \\
Otherwise, let $sg_U=\{u_1, \ldots, u_k\}\subseteq sg$ be a set of literals and $\sigma$ be a 
substitution so that $\sigma$ 
is most general with: $\forall z,
 1\le z\le k: \sigma(\ng u_z)\equiv \sigma(l)$. Moreover, under all subsets of $sg$ and substitutions with
this property, let the set $sg_U$ and the substitution $\sigma$ be a maximum of the function 
$G^{sg}$, defined by 
$G^{sg}(\{u_1,\ldots,u_k\}, \sigma) = \frac{k}{1+ \sum_{z=1}^k |\sigma(u_z)| - |u_z|}$. 
\footnote{$sg_U$ is a rather large set of subgoals that can be solved with $l$ such that not too many 
symbols are introduced by the unifier. This is sensible because otherwise the possibility that the 
remaining subgoals can be solved is decreased too much.}
Then, the remaining literals of $sg$ are $sg_R = \{r_1, \ldots, r_j\} = sg\setminus sg_U$.
Let $\gamma$ be a complexity function, i.e.\ $\gamma$ maps literals to $[0;1]$ and high values of $\gamma$ indicate that the respective literal (subgoal) appears to be solvable. Then,

\[\psi_{BU}^{C, sg}(l) = \sum_{r\in sg_R} \gamma(\sigma(r)) - \sum_{u\in sg_U}
\gamma(\sigma(u)) - j.\]}
\end{definition}

We can recognize that $\psi_{BU}^{C, sg}(l)$ really rates $l$ with a high value if many hard subgoals (w.r.t.\ $\gamma$)
of $sg$ can be
solved with $l$. Moreover, $l$ is rated with a high value if there are only a few subgoals in the
subgoal clause $sg$ that cannot be solved by lemmas and that appear to be solvable rather easily (w.r.t.\ $\gamma$). In our realization, $\gamma$ considers subgoals to be solvable that are small, have a 
rather flat term structure, and many variables in comparison with the term size. In future we will further refine $\psi_{BU}^{C, sg}$ by explicitly
considering the completeness bound which is used for the top-down proof search.


% -------------------------------------------------------------------------------------------------
\section{Experimental Study}
\label{experimente}
In order to conduct an experimental evaluation of our integration of top-down/bottom-up provers,
we coupled two renowned provers: the ME prover \setheo\ and the superposition prover
\spass. We have used the version of \setheo\ as described by \shortciteA{MI97}. \spass\
has been employed in version 0.55.

\subsection{Architecture and Behavior of the Experimental System}
Our experimental environment can be described as follows:
Each prover runs on its own processor and obtains the initial clause set ${\cal C}$ as input. 
We employed a rather efficient method to organize the preprocessing. Essentially, 
the top-down prover generates subgoal clauses with one of the two variants.
In our environment this does not require changes in the top-down prover but can be 
performed with built-ins of the PROLOG-style input language of \setheo. Since \setheo\ employs
$CTC_{{\em neg}}$ we experimented only with subgoal clauses obtained with negative start clauses.
Then, these subgoal clauses are filtered,
transferred to the bottom-up prover, and integrated into its search state. 
The preprocessing of the bottom-up prover is performed in parallel with the preprocessing
of the top-down prover. The prover activates clauses with its basic heuristic until
the top-down prover finishes its preprocessing. Thus, we achieve synchronization of
the provers. After that, we extract the positive
units from the set of active facts of \spass\ and filter some facts as described.
Since we can employ the generated subgoal clauses of \setheo\ for the filter function
$\varphi_{BU}^C$ the generated subgoal clauses can be used as additional input of \spass\
as well as for the selection of lemmas for \setheo.  Finally, the provers proceed to tackle the
problem in parallel with their standard settings.
By using this environment we can achieve cooperation by exchanging lemmas and subgoal clauses without
one concept disturbing the other. In contrast, both concepts support each other because results obtained
from  one preprocessing can be employed in the other.

We experimented in the light of problems stemming from the well-known problem library TPTP v.1.2.1 
\shortcite{SS94,SS98}.  In order to obtain a reliable collection of data, we employed all domains contained in 
the TPTP as our test set. Because these domains cover a wide range of very different problems we assume 
that this is a reliable test set. 

Since the TPTP contains too many problems to list and discuss the runtimes of single
problems, we will present an overview of the number of solved problems
in the TPTP library. Furthermore, we study in which domains cooperation is especially 
important and deal with the main features responsible for this. In addition we study 
the results in three domains in more detail to give an impression for 
the decrease
in run time. This concerns the domains
CAT (category theory), LDA (LD-algebras), and COL (combinatory logic). 
The problems in the domains CAT and LDA contain equality as well as non-Horn clauses.
COL is a Horn-equality domain.

%Since the TPTP contains too many problems to list and discuss runtimes of single
%problems, we want to study the results in three domains in more detail. This concerns the domains
%CAT (category theory), LDA (LD-algebras), and COL (combinatory logic). 
%Note that the problems in the domains CAT and LDA contain equality as well as non-Horn clauses.
%COL is a pure Horn-equality domain.

In detail, the parameters of our experimental system are: 
The subgoal clause candidates were generated in such a way that for variant 1 we employed the 
resource $k=10$ which performed best in the experiments. The use of higher resources did not 
yield better results.  We limited the set of subgoal clauses by $N_{sg}=500$. For variant 2 
we employed $k_1=k_2=9$ as resources. As start clauses for an adaptive refinement we selected $N_{{\em ref}}=5$ subgoal clauses. These parameters allowed the efficient generation of all 
subgoal clauses within the initial segments of the search tree.  Usually with this method at 
most 500 subgoal clauses were generated, i.e.\ about the same number as when employing variant 1. 
For the selection of subgoal clauses that are to be transmitted to \spass\ we used
domain-dependent parameters.  For CAT, COL, and LDA we used 100 clauses. In  the other domains in 
preliminary experiments the use of 30 clauses achieved the best results.

The bottom-up lemmas were selected via the functions $\varphi_{BU}^S$, $\varphi_{BU}^D$, and 
$\varphi_{BU}^C$. We selected with each of the functions a maximum of 10 clauses. 

The setting of \setheo\  was automatically chosen as described by \shortciteA{MI97}.
The \spass\ standard heuristic essentially selects clauses of the smallest size. 
%The size of 
%a clause is computed as a weighted sum of the function
%and variable symbols occurring in the clause. Variables are counted as $1$ and function
%symbols as $2$.  
Periodically, clauses are selected with breadth-first search.


\subsection{Experimental Results}
In the following we compare the results of our cooperative prover with the single provers.
This comparison is performed
regarding the whole TPTP library. After that, we analyze runtimes in few selected domains
of TPTP.

\subsubsection{Comparison of different variants in the TPTP}
Table \ref{tabtptp} presents results of our experiments. It shows the number of solved hard problems 
in certain domains of TPTP. Solved means that a proof could be found within 300 seconds.
We consider a problem to be hard if neither \spass\ nor \setheo\ are able to solve it within 10 seconds.
The table only presents the results of such domains where hard problems exist and where at least
one hard problem could be solved by any of the considered variants. Note that the table 
cannot give hints on the power of the single provers. This is because it does not give the complete
number of problems which can be solved by each single prover in the whole domain. Since many 
non-hard problems are in the TPTP this number is usually much higher than the number of solved hard problems.
Nevertheless, the table is sufficient for analyzing the performance of our cooperative system
since only the hard problems are interesting for studying the
potential of cooperation. 

%\begin{table*}
%\caption{\label{tab1} Integration of top-down/bottom-up approaches by cooperative provers}
%\setlength{\tabcolsep}{3.5pt}
%\begin{center}
%\begin{footnotesize}
%\begin{tabular}{|l|r|r|r|r||l|r|r|r|r|}\hline
%problem & \spass & \setheo & inf.-bas. & adapt. & problem & \spass & \setheo & inf.-bas. & adapt.
%\\ \hline
%\lda{004}{1} & -- & -- & -- & --         &  \cat{001}{1} & -- & -- & -- & -- \\ \hline
%\lda{005}{1} & -- & -- & -- & --         &  \cat{001}{3} & 134s & 32s & 6s & 6s \\ \hline
%\lda{005}{2} & 279s & -- & 265s & 8s     &  \cat{001}{4} & 33s & 11s & 5s & 5s \\ \hline
%\lda{006}{1} & -- & -- & -- & --           &  \cat{002}{2} & -- & -- & -- & -- \\ \hline 
%\lda{006}{2} & 276s & -- & 304s & 10s    &  \cat{003}{1} & -- & -- & -- & -- \\ \hline
%\lda{007}{1} & 16s & 366s & 19s & 21s     &  \cat{004}{3} & -- & 23s & -- & 9s \\ \hline
%\lda{007}{2} & -- & 50s & 7s & 7s         &  \cat{008}{1} & 91s & 126s & 6s & 6s \\ \hline
%\lda{008}{1} & -- & -- & -- & --           &  \cat{009}{1} & -- & -- & 10s & 10s \\ \hline
%\lda{008}{2} & -- & -- & -- & --           &  \cat{009}{3} & -- & -- & -- & 29s \\ \hline
%\lda{009}{1} & -- & -- & -- & --           &  \cat{009}{4} & 53s & -- & 47s & 50s \\ \hline
%\lda{009}{2} & -- & -- & -- & 24s          &  \cat{010}{1} & -- & -- & 11s & 9s \\ \hline
%\lda{010}{1} & -- & -- & -- & 9s           &  \cat{011}{3} & 17s & -- & 12s & 12s \\ \hline
%\lda{010}{2} & -- & -- & -- & 26s          &  \cat{014}{3} & 18s & -- & 11s & 11s \\ \hline
%\lda{011}{1} & 54s & -- & 58s & 9s        &  \cat{018}{3} & -- & -- & -- & 74s \\ \hline
%\lda{011}{2} & 21s & -- & 35s & 7s        &  \cat{019}{4} & -- & -- & -- & -- \\\hline
%\end{tabular}
%\end{footnotesize}
%\end{center}
%\end{table*}

\begin{table}[t]
\setlength{\tabcolsep}{3.5pt}
\begin{center}
%\begin{small}
\begin{tabular}{|l||r|r||r|r||r|r|}\hline
domain & \spass & \setheo & adaptive & lemma & competitive & cooperative \\\hline\hline
ANA & 0 & 2 & 2 & 2 & 2 & 4 \\\hline
BOO & 4 & 3 & 5 & 4 & 5 & 6 \\\hline
CAT & 6 & 4 & 11 & 8 & 7 & 14 \\\hline
CIV & 1 & 0 & 1 & 0 & 1 & 1 \\\hline
COL & 2 & 10 & 2 & 14 & 12 & 16 \\\hline
GEO & 7 & 10 & 8 & 11 & 14 & 15 \\\hline
GRP & 30 & 1 & 36 & 3 & 30 & 38 \\\hline
HEN & 7 & 5 & 9 & 7 & 10 & 12 \\\hline
LCL & 25 & 8 & 26 & 9 & 30 & 31 \\\hline
LDA & 5 & 1 & 9 & 1 & 6 & 9 \\\hline
NUM & 1 & 0 & 1 & 0 & 1 & 1 \\\hline
PLA & 3 & 2 & 3 & 2 & 3 & 3 \\\hline
RNG & 4 & 6 & 4 & 6 & 9 & 9 \\\hline
ROB & 2 & 1 & 3 & 1 & 3 & 3 \\\hline
SET & 21 & 24 & 24 & 35 & 39 & 48 \\\hline
SYN & 0 & 0 & 1 & 0 & 0 & 1 \\\hline\hline
    & 118 & 77 & 145 & 103 & 172 & 211 \\\hline         
\end{tabular}
%\end{small}
\caption{\label{tabtptp} Integration of top-down/bottom-up approaches by cooperative provers: solved hard problems}
\end{center}
\end{table}

Column 1 of the table displays the name of the domain. Columns 2 and 3 present the number of solved problems of
\spass\ and \setheo\ (on a SPARCstation-20/712) when working alone. Column 4 shows the number of solved problems of \spass\
when it obtains subgoal clauses from \setheo\ which are generated regarding variant 2. This variant performs
better than variant 1 (see also the following subsection).
Column 5 displays the number of solved problems of \setheo\ when it obtains bottom-up generated lemmas from \spass. 
In that case we always employed variant 2 for generating subgoal clauses (recall that the selection
of lemmas depends on the way how subgoal clauses are generated). 
Column 6 gives the number of solved problems of a competitive version of \spass\ and \setheo\ 
in order to show that our cooperative prover is indeed much more powerful than
a simple competitive parallel prover. Finally, in column 7 we can find the number of solved problems
 of our cooperative system. 

The results reveal the high potential of our approach to significantly improve on single provers.
\spass\ is only able to solve 55.9\% of the problems which can be solved by cooperation,
\setheo\ can only solve 36.5\%. Competition of provers is very successful because of the very different
behavior of the provers. But even a competitive prover consisting of \spass\ and \setheo\ can only solve
81.5\% of the problems solvable by cooperation. Hence, cooperation is really important in order to 
increase the success rate.
When integrating subgoal clauses into \spass\ its solvability rate is increased by 22.9\%.
In the most cases subgoal clauses take part in the search process and can help to
reorder the search in a favorable manner. The use of lemmas increases \setheo's performance 
by 33.8\%. 
%That is, lemmas are at least as useful as subgoal clauses. 
The increase of the solvability rate of \setheo\ is really due to occurring resource reductions. 
In almost all cases where a substantial speed-up is obtained we could find a proof with a smaller resource. 
Then, the lemmas are used as expected, i.e.\ they are able to close subgoals that occur after few inferences and 
whose ME proof would require many inferences.

When taking a closer look at the results we can recognize the following.
A prover which already shows a rather satisfactory behavior in a specific domain 
can often profit from others.
Cooperation can entail that other hard problems can additionally be
solved. However, if a prover is not suitable for a certain domain then cooperation will normally not result in a significant increase of its performance.
Because of the fact that \setheo\ and \spass\ show a very different
behavior in the most cases at least one prover can be improved
in a certain domain.

It is interesting to find out whether certain characteristics of problems lead to
a high or low performance of the cooperative system. We examine whether the characteristics 
``a domain contains equality'' and ``a domain contains non-Horn problems'' influence the performance.
First, we should note that these characteristics do not completely determine the performance of
the cooperative system. There are gains of efficiency for all kinds of problem, regardless of the 
type of clauses occurring in the problems. But we can at least observe some tendencies. 

Firstly, we can observe that the cooperation approach is especially well-suited
for problems containing equality. The best results are obtained in the domains
CAT, GRP, and SET which contain many problems with equality.
When analyzing proof runs we can find two reasons for this.
In such domains \spass\ is able to support \setheo\ because it has much 
stronger inferences for handling equality than \setheo. \spass\ can often derive
``difficult'' lemmas with few inferences, i.e.\ lemmas whose derivation would require many 
inferences by \setheo. \setheo\ can support \spass\ because it is able to make transformations
of the proof goal that \spass\ cannot perform because of its fixed ordering used for superposition.
This can increase the flexibility of the proof search performed by \spass. 

Secondly, we consider whether the fact that a domain contains mostly Horn or non-Horn
problems influences the performance of the cooperation approach.
Considering the domains where the cooperation approach could successfully be applied
we can notice that successes could be obtained for Horn (e.g., COL) as well as
non-Horn domains (e.g., SET).
In the domains where no hard problems could be solved (neither sequentially nor with
cooperation)
often the percentage of
non-Horn clauses is rather high (note that these domains do not appear in the table). 
The main reason for this, however, appears to be that the single provers show a weak performance in these domains. A strong relationship between the performance of the cooperative 
prover and the fact whether a problem is Horn or non-Horn could not really be found in 
the experiments.

\subsubsection{Analysis of runtimes in selected domains}
Up to now we only considered the number of solved problems. In addition, it is interesting
to analyze whether the use of subgoal  clauses or lemmas can speed-up the proof search in general,
i.e.\ also for problems that can be solved by single provers. Short run times are especially important
if theorem provers are used within interactive prover environments. We restrict ourselves to the three
domains CAT, COL, and LDA and are going to analyze the runtimes in more detail. 

\begin{table*}
%\setlength{\tabcolsep}{3.5pt}
\begin{center}
\begin{footnotesize}
\begin{tabular}{|l||r|r||r|r||r||r|r|}\hline
problem & \spass & \setheo & inference-based & adaptive & lemma & competitive & cooperative \\\hline\hline
\lda{005}{2} & 279s & -- & 265s & 8s & -- & 279s & 8s \\\hline
\lda{006}{2} & 276s & -- & 304s & 10s & -- & 276s & 10s \\\hline
\lda{007}{1} & 16s & 366s & 19s & 21s & 311s & 16s & 21s \\\hline
\lda{007}{2} & -- & 50s & 7s & 7s & 14s & 50s & 7s \\\hline
\lda{009}{2} & -- & -- & -- & 24s & -- & -- & 24s \\\hline
\lda{010}{1} & -- & -- & -- & 9s & -- & -- & 9s \\\hline
\lda{010}{2} & -- & -- & -- & 26s & -- & -- & 26s \\\hline
\lda{011}{1} & 54s & -- & 58s & 9s & -- & 54s & 9s \\\hline
\lda{011}{2} & 21s & -- & 35s & 7s & -- & 21s & 7s \\\hline\hline
\cat{001}{1} & --  & -- & -- & -- & 9s & -- & 9s \\\hline
\cat{001}{3} & 134s & 32s & 6s & 6s & 11s & 32s & 6s \\\hline
\cat{001}{4} & 33s & 11s & 5s & 5s & 6s & 11s & 5s \\\hline
\cat{002}{2} & --  & -- & -- & -- & 98s & -- & 98s \\\hline
\cat{003}{1} & --  & -- & -- & -- & 38s & -- & 38s \\\hline
\cat{004}{3} & -- & 23s & -- & 9s & 10s & 23s & 9s \\\hline
\cat{008}{1} & 91s & 126s & 6s & 6s & 48s & 91s & 6s \\\hline
\cat{009}{1} & -- & -- & 10s & 10s & -- & -- & 10s \\\hline
\cat{009}{3} & -- & -- & -- & 29s & 17s & -- & 17s \\\hline
\cat{009}{4} & 53s & -- & 47s & 50s & -- & 53s & 50s \\\hline
\cat{010}{1} & -- & -- & 11s & 9s & -- & -- & 9s \\\hline
\cat{011}{3} & 17s & -- & 12s & 12s & -- & 17s & 12s \\\hline
\cat{014}{3} & 18s & -- & 11s & 11s & -- & 18s & 11s \\\hline
\cat{018}{3} & -- & -- & -- & 74s & -- & -- & 74s \\\hline\hline
\col{003}{2} & -- & -- & -- & -- & 494s & -- & 494s \\\hline
\col{003}{3} & -- & 60s & -- & -- & 54s & 60s & 54s \\\hline
\col{003}{4} & -- & 19s & -- & -- & 35s & 19s & 35s \\\hline
\col{003}{5} & -- & -- & -- & -- & 100s & -- & 100s \\\hline
\col{003}{7} & -- & 285s & -- & -- & 32s & 285s & 32s \\\hline
\col{003}{9} & -- & 27s & -- & -- & 21s & 27s & 21s \\\hline
\col{034}{1} & -- & 60s & -- & -- & 70s & 60s & 70s \\\hline
\col{036}{1} & -- & 108s & -- & -- & 106s & 108s & 106s \\\hline
\col{037}{1} & -- & 110s & -- & -- & 36s & 110s & 36s \\\hline
\col{038}{1} & -- & 110s & -- & -- & 108s & 110s & 108s \\\hline
\col{041}{1} & -- & 39s & -- & -- & 38s & 39s & 38s \\\hline
\col{042}{2} & -- & -- & -- & -- & 48s & -- & 48s \\\hline
\col{042}{3} & -- & -- & -- & -- & 81s & -- & 81s \\\hline
\col{042}{4} & -- & -- & -- & -- & 52s & -- & 52s \\\hline
\col{057}{1} & -- & 12s & -- & -- & 8s & 12s & 8s \\\hline
\col{060}{1} & 46s & -- & 20s & 20s & -- & 46s & 20s \\\hline
\col{061}{1} & 46s & -- & 17s & 16s & -- & 46s & 16s \\\hline\hline
             & 32.5\% &  40.0\% & 40.0\% & 55.0\% & 62.5\% & 62.5\% & 100\% \\\hline
\end{tabular}
\caption{\label{tab1} Integration of top-down/bottom-up approaches by cooperative provers: runtimes}
\end{footnotesize}
\end{center}
\end{table*}

Table \ref{tab1} presents the runtimes when tackling hard problems of the three test domains.
We omitted all problems that could neither be solved
by a single prover when working alone, nor by any of the cooperation variants.
Column 1 of the table displays the name of the problem. Columns 2 and 3 present the runtimes of
\spass\ and \setheo\ (on a SPARCstation-20/712) when working alone, columns 4 and 5 the runtimes of \spass\
when it obtains subgoal clauses from \setheo\ which are generated regarding variants 1 and 2, respectively. Note that the runtimes
include the generation and selection time of subgoal clauses, and the transmission to \spass.
Column 6 displays the runtime of \setheo\ if it obtains bottom-up generated lemmas from \spass. 
In that case we always employed variant 2 for generating subgoal clauses.
Also these
runtimes include the preprocessing of \spass\ and the transmission and integration of the lemmas.
Column 7 gives the runtime of a competitive version of \spass\ and \setheo\ (minimum of the runtimes
of columns 2 and 3).
Finally, in column 8 we can find the runtime of our cooperative
system (minimum of the runtimes of columns 5 and 6). 
The entry ``--'' means that the problem could not be solved within 1000 seconds.

Since all domains contain equality the results are better than the results
over the whole TPTP.
Our cooperative prover can solve all listed problems, whereas \spass\ is only able to solve 32.5\%,
\setheo\ only 40.0\%. A competitive prover consisting of \spass\ and \setheo\ can merely solve
62.5\% of the problems. 
Not only the success rate but also the runtimes are clearly improved when using a cooperative prover.
The runtimes are often decreased by substantial factors (in spite of the fact that running the 
two provers in parallel consumes twice as much total CPU time).

When studying the runtimes and proofs obtained by \setheo\ we can observe the following. If speed-ups
of \setheo\ are really due to occurring resource reductions, in almost all cases a substantial
speed-up is obtained. Sometimes---for instance in the COL domain---we have the situation
where no resource reduction takes place but reordering effects allow finding proofs faster. 
In this situation, the speed-ups are low. 
Let us take a closer look at the runtimes of \spass\ when using subgoal clauses.
When considering the results of variant 1, the results
show that a naive and uninformed generation of subgoal clauses usually does not entail much gain.
So, only 40\% of the problems can be solved using this variant.
Variant 2, however, shows quite a satisfactory behavior. Hence, an intelligent generation of
a subgoal clause pool really does strongly influence the efficiency.

% -------------------------------------------------------------------------------------------------
\section{Discussion}
\label{disc}
Integration of top-down and bottom-up provers by employing cooperation is very promising in the field of automated
deduction. Due to certain strengths and weaknesses of provers following different paradigms, techniques that try
to combine the strengths by cooperation can allow an improvement of the deductive system.
Our approach of combining top-down and bottom-up provers by processing top-down generated subgoal clauses in a
bottom-up prover achieves this combination by introducing goal-orientation into a bottom-up prover thus combining
strong redundancy control mechanisms and goal-directed search.
The use of bottom-up generated lemmas in a top-down prover can contribute to significantly reduce 
proof lengths such that proofs can be found with smaller resources.

Related approaches for supporting top-down by bottom-up inference also mainly aimed
at employing bottom-up created lemmas in a top-down prover.
Similar to our method 
by \shortciteA{Sch94} and \shortciteA{FuM98b,FuM99} lemmas are created in a preprocessing phase and the 
input clauses are augmented by these formulas.
The main difference of these approaches and our approach is the kind of the used lemmas. There, the ME
inference mechanism is used in order to generate lemmas.
This has the advantage that in some cases---in
contrast to our technique---proof length or resource reductions are guaranteed. However, the lemma
mechanisms used by \shortciteA{FuM98a,FuM98b,FuM99} generate quite ``easy'' lemmas. Hence, their
potential w.r.t.\ the size of the resource reduction is limited. 

Other approaches try to
dynamically create unit lemmas during the proof run of the ME prover \shortcite{AS92,Iw97,AL97}. 
After each successful solution of a subgoal a
lemma might be generated and added to the input clauses.
The aim of this kind of lemma generation is to
produce lemmas that are able to reduce the search amount by eliminating repeated
sub-deductions.
One criticism regarding this kind of lemma generation is the fact that
it is unclear whether or not useful lemmas can be generated. There is no guarantee
that lemmas can be produced during the proof run which can contribute to a proof, 
i.e.\ which can be ``re-used''.
Furthermore, as already mentioned, the generated lemmas are usually not as general as
possible due to instantiations coming from the solutions of subgoals previously
solved.
This can reduce the applicability of a lemma although the
``generalized'' proof could be re-used for refuting the input clauses.
Thus, although some hard problems could only be solved with such lemma techniques \shortcite<see>{AL97}, no
stable success has been reported over a large set of problems.
The main disadvantages of all approaches which only aim at supporting top-down provers 
originate from the
fact that
in some domains, especially if equality is involved, superposition-based provers clearly
outperform ME provers. Thus, in such domains it may be more sensible to develop techniques in order
to support the more powerful bottom-up prover than the weaker top-down prover. 

In order to improve bottom-up proof search by using top-down performed inferences
the following approaches have been employed. Firstly, again one prover (the bottom-up prover) is
assisted by clauses derived from another prover (the top-down prover). 
The approach from \shortciteA{Su92} uses lemmas generated by a guided linear deduction system (and not subgoal clauses) in order to support  
resolution-based provers. Due to the lack of goal orientation (as described in Section \ref{frameworkPreproc})
this method could not yield convincing results in practice.
Secondly, there are approaches to make bottom-up provers more goal-directed by forcing them to work only with some relevant clauses which are detected by top-down calculations.  The methods described by 
\shortciteA{BMSU86}, \shortciteA{St94}, and \shortciteA{Ha97} transform a set of clauses into another clause set which is 
then evaluated in a bottom-up manner. The specific transformation provides a combination of top-down 
and bottom-up processing and prunes the bottom-up evaluation to relevant clauses (which bear 
a connection to a proof goal). Thus, obviously the bottom-up proof search becomes more goal
oriented. Also the method described by \shortciteA{Lov95} provides a relevancy testing for bottom-up calculations. Based on top-down proof attempts the relevancy of a clause is dynamically determined during the bottom-up calculation. In contrast to our method in these approaches the bottom-up prover has to tackle the whole proof task. Our
approach for using top-down generated subgoal clauses in  a bottom-up prover does not provide a
relevancy testing of bottom-up inference but supports the bottom-up inference process by
simplifying the original goal. Thus, the proof length may be shortened. Furthermore,
parts of the
search space of the bottom-up prover, which contain relevant clauses but may be difficult to enumerate, 
can be traversed by a single inference which provides large search reductions.

% -------------------------------------------------------------------------------------------------
\bibliographystyle{theapa}
\bibliography{all}

\end{document}
