@INPROCEEDINGS{C6,
  key    =       {C06},
  AUTHOR =	 {Christoph Benzm{\"u}ller and Volker Sorge},
  TITLE =	 {Critical Agents Supporting Interactive Theorem Proving},
  YEAR =	 1999,
  BOOKTITLE =	 {Progress in Artificial Intelligence, 9th Portuguese Conference
               on Artificial Intelligence, EPIA '99, {\'E}vora, Portugal,
               September 21-24, 1999, Proceedings},
  EDITOR =	 {Pedro Borahona and Jose J.~Alferes},
  PUBLISHER =	 {Springer},
 pages     = {208-221},
  SERIES =	 {LNCS},
  CHRISNOTE =	 {C6},
  number =	 1695,
  URL =		 {www.ags.uni-sb.de/~chris/papers/C6.pdf},
  abstract =	 {We introduce a resource adaptive agent mechanism which supports the user
                  in interactive theorem proving. The mechanism, an extension
                  of~\cite{BeSo98b}, uses a two layered architecture of agent societies to
                  suggest appropriate commands together with possible command argument
                  instantiations. Experiments with this approach show that its
                  effectiveness can be further improved by introducing a resource
                  concept. In this paper we provide an abstract view on the overall
                  mechanism, motivate the necessity of an appropriate resource concept and
                  discuss its realization within the agent architecture.}
}