by Christoph Benzmüller, Andreas Meier, Volker Sorge
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.
Reference:
Bridging Theorem Proving and Mathematical Knowledge Retrieval (Christoph Benzmüller, Andreas Meier, Volker Sorge), Chapter in Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday (Dieter Hutter, Werner Stephan, eds.), Springer, LNCS, volume 2605, pp. 277-296, 2004. (Url (preprint): http://christoph-benzmueller.de/papers/B2.pdf)
Bibtex Entry:
@incollection{B2,
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.},
Author = {Christoph Benzm{\"u}ller and Andreas Meier and
Volker Sorge},
Booktitle = {Mechanizing Mathematical Reasoning: Essays in Honor
of {J{\"o}rg Siekmann} on the Occasion of His 60th
Birthday},
Doi = {10.1007/978-3-540-32254-2_17},
Editor = {Dieter Hutter and Werner Stephan},
Isbn = {978-3-540-25051-7},
Keywords = {own, Proof Assistants, OMEGA, Mathematical Knowledge
Management, System Integration, Interactive Proof},
Pages = {277-296},
Publisher = {Springer},
Series = {LNCS},
Title = {Bridging Theorem Proving and Mathematical Knowledge
Retrieval},
Note = {Url (preprint):
\url{http://christoph-benzmueller.de/papers/B2.pdf}},
Volume = 2605,
Year = 2004,
}