@InCollection{B2,
  key    =       {B02},
  author =	 {Christoph Benzm{\"u}ller and Andreas Meier and Volker Sorge},
  chapter =	 {Bridging Theorem Proving and Mathematical Knowledge Retrieval},
  booktitle =	 {Mechanizing Mathematical Reasoning: Essays in Honor of {J{\"o}rg H. Siekmann} on the Occasion of His 60th Birthday},
  editor =       {Dieter Hutter and Werner Stephan},
  year =	 2004,
  series =	 {LNCS},
  volume =       2605,
  publisher = {Springer},
  pages =        {277-296}, 
  abstract =	 {Accessing knowledge of a single knowledge source with different client
                  applications often requires the help of mediator systems as middleware
                  components. In the domain of theorem proving large efforts have been
                  made to formalize knowledge for mathematics and verification issues, and
                  to structure it in databases. But these databases are either specialized
                  for a single client, or if the knowledge is stored in a general
                  database, the services this database can provide are usually limited and
                  hard to adjust for a particular theorem prover. Only recently there have
                  been initiatives to flexibly connect existing theorem proving systems
                  into networked environments that contain large knowledge bases. An
                  intermediate layer containing both, search and proving functionality can
                  be used to mediate between the two. In this paper we motivate the need
                  and discuss the requirements for mediators between mathematical
                  knowledge bases and theorem proving systems. We also present an attempt
                  at a concurrent mediator between a knowledge base and a proof planning
                  system.}
}