\documentclass[11pt]{article}
\usepackage{a4}
\usepackage{epsfig}
%\usepackage[all]{persmac}
\usepackage{pstricks,pst-node}
\usepackage{proof}
\usepackage{ags-bib}
\usepackage{url}
\usepackage{amssymb}

\scrollmode

\pagestyle{plain}

\def\name#1{{{\sc#1}}}
\def\pcol{{:}}   % Colons in PAIs
\newcommand{\blackboard}[3][3.5cm]{{\scriptsize
    \begin{tabular}{|l|}\hline
      \parbox{#1}{#2}\\\hline
      \\[-.3cm]
      #3
      \hline
    \end{tabular}}}
\def\bfchoice{\mathbf}
\def\A{\bfchoice{A}}\def\B{\bfchoice{B}}\def\C{\bfchoice{C}}\def\D{\bfchoice{D}}
\def\E{\bfchoice{E}}\def\F{\bfchoice{F}}\def\G{\bfchoice{G}}\def\H{\bfchoice{H}}
\def\I{\bfchoice{I}}\def\J{\bfchoice{J}}\def\K{\bfchoice{K}}\def\L{\bfchoice{L}}
\def\M{\bfchoice{M}}\def\N{\bfchoice{N}}\def\O{\bfchoice{O}}\def\P{\bfchoice{P}}
\def\Q{\bfchoice{Q}}\def\R{\bfchoice{R}}\def\S{\bfchoice{S}}\def\T{\bfchoice{T}}
\def\U{\bfchoice{U}}\def\V{\bfchoice{V}}\def\W{\bfchoice{W}}\def\X{\bfchoice{X}}
\def\pred#1{{\mathfrak #1}}
\def\agent{{\mathfrak A}}
\def\cagent{{\mathfrak C}}
\def\commandagent{\cagent}
\def\sagent{{\mathfrak S}}
\def\supportagent{\sagent}
\def\fagent{{\mathfrak F}}
\def\functionagent{\fagent}
\def\gagent{{\mathfrak G}}
\def\goalagent{\gagent}
\def\agentdef#1#2#3#4{{#1}^{\{#2\}}_{{\{#3\}}{,}{\{#4\}}}}
\def\closed{Closed}
\def\lambdot{\rule{0.6mm}{0.6mm}\hspace{0.4ex}}   % the square dot
\def\lamb#1{\lambda #1\lambdot}
\def\all#1{\forall #1\lambdot}
\def\ex#1{\exists #1\lambdot}
\def\exunsymb{\exists!}
\def\exunique#1{\exunsymb #1\lambdot}
\def\sdot{\rule{.3ex}{.3ex}\hskip.1ex}
\def\classres{Res}
\def\congclass{cl}
\def\RSsymb{RS}
\def\RS#1{\RSsymb_{#1}}
\def\srsn#1{\ensuremath \vbar{#1}{:}{\scriptstyle RS_n}}
\def\sort#1#2{\ensuremath #1{:}{\scriptstyle #2}}
\def\resclass#1#2{\ensuremath \congclass_{#1}(#2)}
\def\sisn#1#2{\ensuremath \vbar{#1}{:}{\scriptstyle\Int_{#2}}}
\def\vbar#1{\ensuremath #1}
\def\resplus{\bar{+}}
\def\restimes{\bar{*}}
\def\resminus{\bar{-}}
\def\wff{{\bf wff}}
\def\wsf{{\bf wsf}}
\def\Func{{{\cal F}}}
\def\Univ{{{\cal U}}}
\def\wahr{{\mbox{\sf t}}}
\def\falsch{{\mbox{\sf f}}}
%\def\true{{\wahr}}
%\def\false{{\falsch}}
\def\omicron{{o}}
\def\impl{{\Rightarrow}}
\def\implies{\Rightarrow}
\def\eqv{\Leftrightarrow}
\def\equal{{\;=\;}}
\def\defiff{{{\rm gdw.}}}
\def\ohne{{\backslash}}
\def\absatz#1{{\vspace*{#1ex}}}
\def\tuple#1{{\left\langle #1 \right\rangle}}
\def\menge#1{{\left\{ #1 \right\}}}
\def\leeremenge{{\emptyset}}
\def\emptylist{{\tuple{ \mbox{} }}}
\def\emptysubst{{\{ \mbox{} \}}}
\def\emptypos{{[ \mbox{} ]}}
\def\leerobj#1{{empty(\sort{#1})}}
\def\conv{{\con}}
\def\assert{{\ensuremath{Assertion}}}
\def\applyass{\ensuremath{ApplyAss}}
\def\reduceclosed{\ensuremath{ReduceClosed}}
\def\inint{\ensuremath{InInt}}
\def\inresclset{\ensuremath{InResclSet}}
\def\OANTS{\mbox{$\Omega$-{\sc Ants}}}
\newcommand{\Int}{{\mathchoice{\displaystyle\rm \rm Z\hskip-0.32em Z}%
{\textstyle\rm \rm Z\hskip-0.32em Z}%
{\scriptstyle\rm \rm Z\hskip-0.22em Z}%
{\scriptscriptstyle\rm \rm Z\hskip-0.22em Z}}}
\def\OMEGA{{$\Omega${\sc mega}}}

\begin{document}

\title{Distributed Assertion Retrieval} 

\author{Christoph Benzm\"uller, Andreas Meier and Volker Sorge\\
\small Fachbereich Informatik\\
\small Universit\"at des Saarlandes\\
\small D-66041 Saarbr\"ucken, Germany\\ 
\small \{chris$|$ameier$|$sorge\}@ags.uni-sb.de\\
\small http://www.ags.uni-sb.de/\~{}\{chris$|$ameier$|$sorge\}
}

\date{}


\maketitle

\section{Motivation}
\name{Huang} has identified the {\em assertion level} as a well defined abstraction level for natural
deduction proofs~\cite{Huang94phd,Huang94}. Proofs at assertion level are composed of the direct application
of assertions, like theorems, axioms, and definitions.

To clarify the notion of assertion application we pick one of \name{Huang}'s examples as given
in~\cite{Huang94}. An assertion application is for instance the application of the $SubsetProperty$ 
 \[\all{S_1}\all{S_2}S_1\subset S_2\equiv\all{x}x\in S_1\implies x\in S_2\] in the following way:
\[\infer[\assert(SubsetProperty)]{a\in F}{\;a\in U & U\subset F\;}\] The direct application of the assertion
is thus an abbreviation for a more detailed reasoning process on the calculus level; that is, the explicit
derivation of the goal $a\in F$ from the two premises by appropriately instantiating and splitting the
$SubsetProperty$ assertion.

In the {\OMEGA} system~\cite{Omega97} assertions are applied using a specialized $\assert$ tactic. Its purpose
is to derive a goal from a set of premises with respect to a theorem or axiom. It thus enables the more
abstract reasoning with respect to given assumptions at the assertion level. We can depict the assertion
tactic as a general inference rule in the following way
\[\infer[\assert(Ass)]{Goal}{\;Prems\;}\]
where $Prems$ is a list of premises, $Goal$ is the conclusion and $Ass$ is the assertion that is applied.

Determining possible assertion applications for subsequent subgoals in a proof attempt can easily become a
very difficult task and a direct, sequential interleaving of assertion applicability tests with the main
theorem proving loop is a rather ineligible option. 
 
Firstly, there might be too many assertions in the database to be checked sequentially in each proof step.
This motivates a concurrent mechanism; optimally one with any-time behavior, that allows to continue the
proving process regardless of termination of applicability checks for assertions but also to resume those
checks if necessary.

Secondly, each applicability check might call for costly, complex, and probably even undecidable algorithms.
One problem is that an assertion or a succedent of an assertion might not directly match with a focused open
subgoal such that some deduction steps are needed to establish the applicability. For instance, if a
mathematical database entails a theorem of the form $\A_1 \wedge \ldots \wedge \A_n \implies (\B
\Leftrightarrow \C)$ while the focused subgoal is $\C \Leftrightarrow \B$, then symmetry of $\Leftrightarrow$
is crucial for the applicability of the theorem. Thus, in its most general form the task of determining
applicable assertions entails some, more or less restricted, theorem proving as an undecidable side condition.
In a higher-order theorem proving environment (e.g., {\OMEGA} is based on a higher order natural deduction
variant, and thus higher order assertions and proof goals do occur) even matching is already complex and
generally undecidable\footnote{Decidability of full higher-order matching is still an open question.}. On the
other hand many applicable assertions can already be detected by much simpler algorithms such as first-order
matching.  This motivates a flexible and parameterizable assertion retrieval mechanism, where simple,
efficient algorithms as well as powerful, complex ones can be concurrently employed in a resource adapted
manner.
 
Thirdly, assertion retrieval should not rely on database dependend specifics such as theory names or even
assertion names. For instance, in some {\OMEGA} proof methods such specific knowledge is employed to precisely
search for respective assertions. However, this database dependend knowledge contrasts robustness of assertion
retrieval as slight modification of the database may compromise the success of these methods. It also
contrasts the possibility of interoperatibility with alternative databases.

In order to meet the above requirements we suggest a technique to separate the search for applicable
assertions from the the main proving process and to supersede database dependencies by general search
criterions. Our approach, which employs the {\OANTS} blackboard mechanism~\cite{BeSo99b,BeSo01}, serves for
both automated (e.g., with {\OMEGA}'s proof planner) and interactive theorem proving. The idea is to view the
applicability tests as little independent and resource bounded processes that run in parallel in the
background. This especially enables us to employ powerful and even undecidable algorithms without directly
affecting the main theorem proving process in the foreground. Applicable theorems are dynamically signaled to
the prover including information which particular subgoal is addressed. Thus, whenever the prover is
determining which step to perform next it can take these options into account -- this holds for new open
subgoals as well as for re-opened, backtracked subgoals in the proof process.

% Our work tasks are:
% \begin{description}
% \item[Modeling] to investigate how {\OANTS} can be adapted to support also the search for applicable
%   assertions,
% \item[Evaluation] to evaluate the mechanisms performance; for instance to relate it to indexing based
%   retrieval techniques, and
% \item[Integration] to integrate the approach with services provided by mathematical databases
%   such as Mizar~\cite{TrBl85} or MBASE~\cite{FrKo99mbase}.
% \end{description}


\section{Modeling Assertion Retrieval in \OANTS} 

{\OANTS}~\cite{BeSo99b} is a blackboard architecture that was originally developed to compute applicable
inference rules in interactive and automated theorem proving. In this context inference rules (e.g., calculus
rule, tactics, or planning methods) are uniformly regarded as sets of premises, conclusions and additional
parameters. The elements of these three sets comprise the arguments of an inference rule and have generally
certain dependencies amongst each other. In order for an inference rule to be applicable at least some of its
arguments have to be instantiated with respect to the given proof context. The task of the {\OANTS}
architecture is now to determine the applicability of inference rules by computing instantiations for their
arguments. The architecture consists of two layers: The upper layer collects and evaluates data on
instantiations of arguments for the given inference rules and thereby compiles a set of applicable rules. This
information is computed on the lower layer of the architecture concurrently for each inference rule. The lower
layer consists of single societies of agents, one society for each inference rules. These agents are
independent processes that cooperatively compute argument instantiations with respect to the current proof
state. {\OANTS} provides facilities to define and modify its distributed processes at run-time and also
facilities to employ resource reasoning to guide the search.

We currently examine an approach to model assertion retrieval in {\OANTS}, which distributes the applicability
checks for assertions to several agents. These agents are arranged in agent societies realizing the following
two principles: (1) Each agent society is able to check a certain cluster of assertions. (2) Within an agent
society the checks are done in two phases: first a filter agent performs a simple check, then further retrieval
agents employ more fine grained, but probably more expensive applicability checks. The cluster of assertions
associated with an agent society consists of related assertions applicable to subgoals that share a certain
property which is simple to test. This test is performed by the filter agent of the society. The retrieval agents
of a society employ then different further applicability checks such as first order matching, higher order
matching, or even full higher order theorem proving. This separation of preselection and main check enables
the exclusion of many available assertions already by rather simple tests without having to carry out all
possible matchings and unifications.

During the proof process, for an open subgoal first the filter agents identify
promising theorem clusters. For societies whose
filter agent succeeds the retrieval agents become active. If successfull, these agents provide suggestions about
assertions that are applicable to the open subgoals. When there is a suggestion about an applicable assertion
a further agent, called premise agent, is triggered which tries to identify whether the proof context already contains support
lines that can be employed to justify the premises of the assertion. This premise agent is also part of every
agent society.  With the information computed for the single agent societies {\OANTS} can compile a set of
applicable assertions on the top level and suggest them to the prover. Each individual suggestion contains
information on the investigated subgoal, an identified applicable assertion, and available support lines that
can be used immediately to weaken premises of the assertion.

Note, that the cluster of assertions associated with an agent society is formed dynamically at run-time.
Technically, this is realized by equipping the retrieval agents with specifications, about which assertions the
agent can process. Then at run-time the retrieval agents first look-up the data-base of assertions and form the
clusters of assertions associated with the different agent societies, respectively.  Selecting the assertions
via specifications enables a more refined selection of assertions and makes this selection independent of
explicit references to assertions or a particular data-base. Furthermore, new assertions can be dynamically
added and fitted into the existing clusters.

%We currently examine an approach to model assertion retrieval in {\OANTS}, which decomposes the applicability
%tests for assertions into sequences of tests. These tests are realized by independent agents. For instance,
%different agents can incorporate different matching algorithms. At run-time these agents dynamically form
%societies, where each society cooperatively tests a certain cluster of related assertions on applicability.
%For instance, a cluster can contain theorems that are all concerned with a particular property. Then we can
%preselect according to the given goal whether the theorems of a given cluster could be successfully matched
%without having to carry out all possible matchings.  Selecting the theorems via specifications enables a more
%refined selection of theorems and makes this selection independent of explicit reference to theorems.
%Furthermore, new theorems can be dynamically added and fitted into the existing clusters.
%
%All clusters are of a similar composition and the retrieval of applicable theorems in a cluster is realized in
%{\OANTS} analogously for all clusters.  Given an open subgoal in the proving process each cluster property is
%checked by a respective agent working for this cluster.  This gives a first simple, yet effective, filter for
%reducing the number of considered theorems. For each cluster that passed this first filter further agents
%become active, which now employ more fine grained, but probably more expensive applicability checks such as
%first order matching, higher order matching, or even full higher order theorem proving. For each applicable
%theorem then another agent becomes active which tries to identify whether the proof context already contains
%support lines that can be employed to justify the premises of the theorem. With the information computed for
%the single clusters {\OANTS} can compile a set of applicable theorems on the top level and suggest them to the
%prover. Each individual suggestion contains information on the investigated subgoal, an identified applicable
%theorem, and available support lines that can be used immediately to weaken premises of the theorem.

\section{Example}

Our example is taken from a case study on the proofs of properties of residue classes. In this case study
we apply {\OMEGA}'s proof planner to classify residue class sets over the integers together with given binary operations 
in terms of their basic algebraic properties. The case study is described in detail in~\cite{MePoSo01}. We concentrate here 
on how {\OANTS} determines the applicability of assertions in this context. 
We consider the first step in the proof of the theorem\vspace{-.2cm}
\[Conc.\;\vdash \closed(\Int_5,\lamb{\vbar{x}}\lamb{\vbar{y}}(\vbar{x}\restimes\vbar{y})\resplus\bar{3}_5).\vspace{-.2cm}\] 
It states that the given residue class set $\Int_5$ is closed with respect to the operation
$\lamb{\vbar{x}}\lamb{\vbar{y}}(\vbar{x}\restimes\vbar{y})\resplus\bar{3}_5$. Here $\Int_5$ is the set 
of all congruence classes modulo $5$, i.e., $\{\bar{0}_5,\bar{1}_5,\bar{2}_5,\bar{3}_5,\bar{4}_5\}$. $\restimes$ and $\resplus$
are the multiplication and addition on residue classes. 

Among the theorems we have for the domain of residue classes there are some that are concerned with statements
on the closure property. In particular, we have the following six theorems:

\vspace*{0.2cm}
$\begin{array}{ll}
  \hspace{-.5cm}ClosedConst: & \all{\sort{n}{\Int}}\all{\sort{c}{\Int_n}}\closed(\Int_n,\lamb{\vbar{x}}\lamb{\vbar{y}}c)\\
  \hspace{-.5cm}ClosedFV: & \all{\sort{n}{\Int}}\closed(\Int_n,\lamb{\vbar{x}}\lamb{\vbar{y}}\vbar{x})\\
  \hspace{-.5cm}ClosedSV: & \all{\sort{n}{\Int}}\closed(\Int_n,\lamb{\vbar{x}}\lamb{\vbar{y}}\vbar{y})\\
  \hspace{-.5cm}ClComp\resplus: & \all{\sort{n}{\Int}}\all{op_1}\all{op_2}(\closed(\Int_n,op_1) \wedge \closed(\Int_n,op_2)) \implies\quad\quad\quad\\
    & \hspace*{3.5cm}\closed(\Int_n,\lamb{\vbar{x}}\lamb{\vbar{y}}(\vbar{x}\ op_1\ \vbar{y}) \resplus (\vbar{x}\ 
  op_2\ \vbar{y}))\\
  \hspace{-.5cm}ClComp\resminus: & \all{\sort{n}{\Int}}\all{op_1}\all{op_2}(\closed(\Int_n,op_1) \wedge \closed(\Int_n,op_2)) \implies\quad\quad\quad\\
    & \hspace*{3.5cm}\closed(\Int_n,\lamb{\vbar{x}}\lamb{\vbar{y}}(\vbar{x}\ op_1\ \vbar{y}) \resminus (\vbar{x}\ 
  op_2\ \vbar{y}))\\
  \hspace{-.5cm}ClComp\restimes: & \all{\sort{n}{\Int}}\all{op_1}\all{op_2}(\closed(\Int_n,op_1) \wedge \closed(\Int_n,op_2)) \implies\quad\quad\quad\\
    & \hspace*{3.5cm}\closed(\Int_n,\lamb{\vbar{x}}\lamb{\vbar{y}}(\vbar{x}\ op_1\ \vbar{y}) \restimes (\vbar{x}\ 
  op_2\ \vbar{y}))
\end{array}$

\vspace*{0.2cm} The theorems $ClosedConst$, $ClosedFV$, and $ClosedSV$ talk about residue class sets with
simple operations whereas $ClComp\resplus$, $ClComp\resminus$, and $ClComp\restimes$ are concerned with
combinations of complex operations. The difference between the groups of theorems is that the applicability of
former can be checked with slightly adapted first order matching whereas for the latter we need higher order
matching. For example, when applying the theorem $ClComp\resplus$ to our problem at hand the required
instantiations are $op_1\leftarrow\lamb{\vbar{x}}\lamb{\vbar{y}}\vbar{x}\restimes\vbar{y}$ and
$op_2\leftarrow\lamb{\vbar{x}}\lamb{\vbar{y}}\bar{3}_5$, which cannot be found by first order matching.
However, since we are concerned with only a distinct set of binary operations and their combinations, we can
keep things decidable by using a special, decidable algorithm, which matches the statements of the theorems
$ClComp\resplus$, $ClComp\resminus$, and $ClComp\restimes$ with nested operations on congruence classes.

\begin{figure}[t]
  \begin{center}
    \begin{tabular}{|p{10.2cm}|}\hline
      \begin{center}\vspace{-1em}
        $
        \begin{array}{lcl} 
          \gagent &\hspace{-.1cm} {=}\hspace{-.1cm} & 
          \{ \mbox{\footnotesize $Goal$: $Goal$ contains the $\closed$ predicate}\}\\[.2cm]
          \fagent_1 &\hspace{-.1cm} {=}\hspace{-.1cm} & 
          \{ \mbox{\footnotesize $Thm$: Conclusion matches $Goal$ with first order matching} \}
          \hspace*{-.2cm} \\
          &&\begin{minipage}{8.5cm}
            $\left\{ \mbox{\footnotesize
                \begin{tabular}{ll}
                  \hspace*{-.3cm}$Acquisition$: & \hspace*{-.3cm}Conclusion contains $\closed$ as outermost \\
                  & \hspace*{-.3cm}predicate and a constant operation
                \end{tabular}}\right\}$
          \end{minipage}
          \hspace*{-.2cm} \\[.2cm]
          \fagent_2 &\hspace{-.1cm} {=}\hspace{-.1cm} & 
          \{ \mbox{\footnotesize $Thm$: Conclusion matches $Goal$ with special algorithm} \}\\
          &&\begin{minipage}{8.5cm}
            $\left\{ \mbox{\footnotesize
                \begin{tabular}{ll}
                  \hspace*{-.3cm}$Acquisition$: & \hspace*{-.3cm}Conclusion contains $\closed$ as outermost \\
                  & \hspace*{-.3cm}predicate and a binary operation
                \end{tabular}}\right\}$
          \end{minipage}\\[.2cm]
          \sagent &\hspace{-.1cm} {=}\hspace{-.1cm} & 
          \{\mbox{\footnotesize $Prem$: The nodes matching the premises of $Thm$}\}
        \end{array}
        $
      \end{center}\\\hline
    \end{tabular}
    \caption{Agent society for the $\closed$ theorem cluster.}
    \label{fig:closed-agents}
  \end{center}
  \vspace*{-0.7cm}
\end{figure}

In {\OANTS} we have the agent society as depicted in Figure~\ref{fig:closed-agents} for the cluster comprising
the theorems given above. The filter agent $\gagent$ searches for possible conclusions that contain an
occurrence of the $\closed$ predicate.  $\gagent$ writes respective suggestions of goals to the blackboard.
We then have two retrieval agents, $\fagent_1$ and $\fagent_2$, that try to match the theorems. $\fagent_1$ tries to
match the theorems $ClosedConst$, $ClosedFV$, and $ClosedSV$ to the formulas suggested by $\gagent$ using
first order matching.  $\fagent_2$ uses the special algorithm instead of matching the theorems
$ClComp\resplus$, $ClComp\resminus$, and $ClComp\restimes$ conventionally. $\fagent_1$ and $\fagent_2$ have
additional acquisition predicates specifying that the agents can acquire theorems whose conclusions have
$\closed$ as the outermost predicate. $\fagent_1$ furthermore requires that the theorem conclusion contains a
simple, constant operation while $\fagent_2$ expects a complex operation.  The acquisition predicate serves to
retrieve appropriate theorems from the knowledge base initially and dynamically at run-time if new theorems
are added. For each applicable theorem they detect $\fagent_1$ and $\fagent_2$ place new extended suggestions
on the blackboard. The last agent is the premise agent $\sagent$, which has an algorithm to extract the necessary
premises from a theorem suggested by $\fagent_1$ or $\fagent_2$ and, if there are any, tries to find
appropriate proof lines containing them.

For our concrete example theorem the information that accumulates on the command blackboard for the $\closed$
theorem cluster is as follows:%\vspace*{-.1cm}
\begin{center}\hspace*{-.5em}
  \begin{tabular}{p{3.1cm}p{3.7cm}p{5.1cm}}\hspace{-.3cm}
    \Rnode{bb2a}{\blackboard[2.2cm]{$\closed$}{\\\\\\\\}}
    &
    \Rnode{bb2b}{\blackboard[2.6cm]{$\closed$}{$(Goal\pcol Conc)$\\\\\\\\}}
    &
    \Rnode{bb2c}{\blackboard[3.2cm]{$\closed$}{$(Goal\pcol Conc)$\\
        $(Goal\pcol Conc, Thm\pcol ClComp\resplus)$\\ 
        \\\\}}
  \end{tabular}\hspace*{-2em}
  \ncline[arrows=->]{bb2a}{bb2b}
  \ncline[arrows=->]{bb2b}{bb2c}
\end{center}\vspace*{-.1cm}

First $\gagent$ detects an occurrence of the $\closed$ predicate in the given goal $Conc$ and adds an entry
suggesting it as instantiation for $Goal$ to the blackboard. With this entry the $\fagent_1$ and $\fagent_2$
start matching their respective theorems to $Conc$. $\fagent_2$ is successful with the $ClComp\resplus$
theorem and adds the matched theorem as suggestion. Then $\sagent$ starts its search; for our example it is
looking for premises of the form $\closed(\Int_5,\lamb{\vbar{x}}\lamb{\vbar{y}}\bar{3}_5)$ and
$\closed(\Int_5,\lamb{\vbar{x}}\lamb{\vbar{y}}\vbar{x} \restimes \vbar{y})$.

\section{Outlook}

\paragraph{Evaluation:}
An important aspect of our work will be to evaluate our current modeling of goal directed theorem retrieval in
{\OANTS} and also to relate them to both other possible modeling approaches in {\OANTS} and standard
indexing techniques.

A disadvantage of our current approach is that the predicates for forming clusters as well as some of the
agents for matching assertions have to be explicitely specified. This could be avoided if each theorem is
directly identified with an {\OANTS} agent that analyzes the theorem's applicability. However, this approach
essentially only distributes the complete testing of all assertions without effectively reducing the number
and complexity of the tests. Nevertheless, a thorough comparison between the two different approaches should
be made.

Compared with standard indexing techniques our viewpoint of theorem retrieval goes beyond their capabilities.
Indexing techniques rely typically on decidable matching or unification contexts.  Generally our mechanism
aims at the retrieval of theorems modulo more powerful filters as well.  Apart from standard matching or
unification filters we also employ full theorem proving.  Additionally the checks for different theorems are
executed in parallel.  These processes are controlled and bounded by the resource concepts of {\OANTS}.
Moreover we make use of {\OANTS} anytime character that allows to apply suggested theorems without waiting for
all applicability checks to have finished.

\paragraph{Integration:}
In the long run we aim to integrate our approach with the services provided by a mathematical database like
Mizar~\cite{TrBl85} or MBASE~\cite{FrKo99mbase}. MBASE, for example, already supports simple queries based on
first order matching to retrieve theorems which are applicable to a subgoal at hand.  More powerful query
services are planned but it is clear that there will be limits. For instance, to employ full higher order
theorem proving within the retrieval of theorems is out of reach for a mathematical knowledge base project.
Here is where both approaches can be merged. Simple filter queries, for instance the test of cluster
properties, can probably be successfully mapped to database services from within the {\OANTS} agents. More
powerful methods, such as theorem provers, should be employed in {\OANTS} making use of the distribution and
resource mechanisms.

\small
%\bibliography{lit}
\bibliographystyle{plain}
\begin{thebibliography}{1}

\bibitem{Omega97}
C.~Benzm{\"u}ller, L.~Cheikhrouhou, D.~Fehrer, A.~Fiedler, X.~Huang, M.~Kerber,
  M.~Kohlhase, K.~Konrad, E.~Melis, A.~Meier, W.~Schaarschmidt, J.~Siekmann,
  and V.~Sorge.
\newblock {$\Omega$Mega}: {T}owards a {M}athematical {A}ssistant.
\newblock In {\em {\PROC} of CADE--14}, volume 1249 of {\em \LNAI}, pages
  252--255. Springer Verlag, 1997.

\bibitem{BeSo99b}
C.~Benzm{\"u}ller and V.~Sorge.
\newblock {Critical Agents Supporting Interactive Theorem Proving}.
\newblock In {\em {\PROC} of EPIA-99}, volume 1695 of {\em \LNAI}, pages
  208--221. Springer Verlag, 1999.

\bibitem{BeSo01}
C.~Benzm{\"u}ller and V.~Sorge.
\newblock {\OANTS} -- an open approach at combining interactive and automated
  theorem proving.
\newblock In {\em {\PROC} of the Calculemus Symposium 2000}. AK Peters, 2001.

\bibitem{FrKo99mbase}
A.~Franke and M.~Kohlhase.
\newblock {MBase: Representing mathematical Knowledge in a Relational Data
  Base}.
\newblock In {\em {CALCULEMUS 99}, Systems for Integrated Computation and
  Deduction}, Electronic Notes in Theoretical Computer Science, pages 135--152.
  Elsevier, 1999.

\bibitem{Huang94phd}
X.~Huang.
\newblock {\em {H}uman {O}riented {P}roof {P}resentation: {A} {R}econstructive
  {A}pproach}.
\newblock PhD thesis, \FBI, \UdS\GERMANY, 1994.

\bibitem{Huang94}
X.~Huang.
\newblock {R}econstructing {P}roofs at the {A}ssertion {L}evel.
\newblock In {\em {\PROC} of CADE--12}, volume 814 of {\em \LNAI}, pages
  738--752. Springer Verlag, 1994.

\bibitem{MePoSo01}
A.~Meier, M.~Pollet, and V.~Sorge.
\newblock {Classifying Isomorphic Residue Classes}.
\newblock In {\em {\PROC} of EuroCAST 2001}, volume 2178 of {\em \LNCS}.
  Springer Verlag, 2001.

\bibitem{TrBl85}
A.~Trybulec and H.~Blair.
\newblock Computer assisted reasoning with {MIZAR}.
\newblock In {\em {\PROC} of the 9th International Joint Conference on
  Artificial Intelligence}, pages 26--28. Morgan Kaufmann, 1985.

\end{thebibliography}



\end{document}
