Bridging Theorem Proving and Mathematical Knowledge Retrieval

Bridging Theorem Proving and Mathematical Knowledge Retrieval. Benzmüller, C., Meier, A., & Sorge, V. In Hutter, D. & Stephan, W., editors, Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday, volume 2605, of LNCS, pages 277-296. Springer, 2004.

Preprint doi abstract bibtex

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.

@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},
  url_preprint = {http://christoph-benzmueller.de/papers/B2.pdf},
  Volume =	 2605,
  Year =	 2004,
}

Downloads: 0

{"_id":"oKSsTGitrd57puM7P","bibbaseid":"benzmller-meier-sorge-bridgingtheoremprovingandmathematicalknowledgeretrieval-2004","author_short":["Benzmüller, C.","Meier, A.","Sorge, V."],"bibdata":{"bibtype":"incollection","type":"incollection","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":[{"firstnames":["Christoph"],"propositions":[],"lastnames":["Benzmüller"],"suffixes":[]},{"firstnames":["Andreas"],"propositions":[],"lastnames":["Meier"],"suffixes":[]},{"firstnames":["Volker"],"propositions":[],"lastnames":["Sorge"],"suffixes":[]}],"booktitle":"Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday","doi":"10.1007/978-3-540-32254-2_17","editor":[{"firstnames":["Dieter"],"propositions":[],"lastnames":["Hutter"],"suffixes":[]},{"firstnames":["Werner"],"propositions":[],"lastnames":["Stephan"],"suffixes":[]}],"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","url_preprint":"http://christoph-benzmueller.de/papers/B2.pdf","volume":"2605","year":"2004","bibtex":"@incollection{B2,\n Abstract =\t {Accessing knowledge of a single knowledge source\n with different client applications often requires\n the help of mediator systems as middleware\n components. In the domain of theorem proving large\n efforts have been made to formalize knowledge for\n mathematics and verification issues, and to\n structure it in databases. But these databases are\n either specialized for a single client, or if the\n knowledge is stored in a general database, the\n services this database can provide are usually\n limited and hard to adjust for a particular theorem\n prover. Only recently there have been initiatives to\n flexibly connect existing theorem proving systems\n into networked environments that contain large\n knowledge bases. An intermediate layer containing\n both, search and proving functionality can be used\n to mediate between the two. In this paper we\n motivate the need and discuss the requirements for\n mediators between mathematical knowledge bases and\n theorem proving systems. We also present an attempt\n at a concurrent mediator between a knowledge base\n and a proof planning system.},\n Author =\t {Christoph Benzm{\\\"u}ller and Andreas Meier and\n Volker Sorge},\n Booktitle =\t {Mechanizing Mathematical Reasoning: Essays in Honor\n of {J{\\\"o}rg Siekmann} on the Occasion of His 60th\n Birthday},\n Doi =\t\t {10.1007/978-3-540-32254-2_17},\n Editor =\t {Dieter Hutter and Werner Stephan},\n Isbn =\t {978-3-540-25051-7},\n Keywords =\t {own, Proof Assistants, OMEGA, Mathematical Knowledge\n Management, System Integration, Interactive Proof},\n Pages =\t {277-296},\n Publisher =\t {Springer},\n Series =\t {LNCS},\n Title =\t {Bridging Theorem Proving and Mathematical Knowledge\n Retrieval},\n url_preprint = {http://christoph-benzmueller.de/papers/B2.pdf},\n Volume =\t 2605,\n Year =\t 2004,\n}\n\n","author_short":["Benzmüller, C.","Meier, A.","Sorge, V."],"editor_short":["Hutter, D.","Stephan, W."],"key":"B2","id":"B2","bibbaseid":"benzmller-meier-sorge-bridgingtheoremprovingandmathematicalknowledgeretrieval-2004","role":"author","urls":{" preprint":"http://christoph-benzmueller.de/papers/B2.pdf"},"keyword":["own","Proof Assistants","OMEGA","Mathematical Knowledge Management","System Integration","Interactive Proof"],"metadata":{"authorlinks":{}}},"bibtype":"incollection","biburl":"http://page.mi.fu-berlin.de/cbenzmueller/papers/chris.bib","dataSources":["ckRabafyoGpACyPpf","S5G7BggtbXZA2Q63T"],"keywords":["own","proof assistants","omega","mathematical knowledge management","system integration","interactive proof"],"search_terms":["bridging","theorem","proving","mathematical","knowledge","retrieval","benzmüller","meier","sorge"],"title":"Bridging Theorem Proving and Mathematical Knowledge Retrieval","year":2004}