@InProceedings{C8,
  key    =       {C08},
  author =	 {Christoph Benzm{\"u}ller and Volker Sorge},
  title =	 {{OANTS} -- An open approach at combining Interactive and Automated Theorem
                  Proving},
  booktitle =	 {Symbolic Computation and Automated Reasoning},
  editor =       {Manfred Kerber and Michael Kohlhase},
  year =	 2000,
  pages =        {81--97},
  publisher =	 {A.K.Peters},
  url =		 {www.ags.uni-sb.de/~chris/papers/C8.pdf},
  abstract =	 {We present the O-ANTS theorem prover that is built on top of an
                  agent-based command suggestion mechanism. The theorem prover inherits
                  beneficial properties from the underlying suggestion mechanism such as
                  run-time extendibility and resource adaptability. Moreover, it supports
                  the distributed integration of external reasoning systems. We also
                  discuss how the implementation and modeling of a calculus in our
                  agent-based approach can be investigated wrt. the inheritance of
                  properties such as completeness and soundness.}
}