Skip to main content
SpringerLink
Log in

Bridging Theorem Proving and Mathematical Knowledge Retrieval

  • Chapter
Book cover Mechanizing Mathematical Reasoning

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2605))

  • 1062 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, P.B., Bishop, M., Brown, C.E.: TPS: A theorem proving system for type theory. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 164–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Anonymous. The qed manifesto. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 238–251. Springer, Heidelberg (1994)

    Google Scholar 

  3. Armando, A., Zini, D.: Towards interoperable mechanized reasoning systems: the logic broker architecture. In: Poggi, A. (ed.) Proceedings of the AI*IA-TABOO Joint Workshop From Objects to Agents: Evolutionary Trends of Software Systems, Parma, Italy (2000)

    Google Scholar 

  4. Baumgartner, P., Furbach, U.: PROTEIN: A prover with a theory extension interface. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 769–773. Springer, Heidelberg (1994)

    Google Scholar 

  5. Benzmüller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Melis, E., Meier, A., Schaarschmidt, W., Siekmann, J., Sorge, V.: ΩMega: Towards a Mathematical Assistant. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 252–255. Springer, Heidelberg (1997)

    Google Scholar 

  6. Benzmüller, C., Bishop, M., Sorge, V.: Integrating tps and Ωmega. Journal of Universal Computer Science 5(3), 188–207 (1999); Special issue on Integration of Deduction System

    Google Scholar 

  7. Benzmüller, C., Sorge, V.: Critical Agents Supporting Interactive Theorem Proving. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol. 1695, pp. 208–221. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Bishop, M., Andrews, P.: Selectively instantiating definitions. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 365–380. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between CLAM and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 87–104. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  10. Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. Journal of Automated Reasoning 7, 303–324 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  11. Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  12. Calmet, J., Jekutsch, S., Kullmann, P., Schü, J.: KOMET: A system for the integration of heterogenous information sources. In: Raś, Z.W., Skowron, A. (eds.) ISMIS 1997. LNCS, vol. 1325. Springer, Heidelberg (1997)

    Google Scholar 

  13. Dahn, B.I., Gehne, J., Honigmann, T., Wolf, A.: Integration of automated and interactive theorem proving in ilf. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 57–60. Springer, Heidelberg (1997)

    Google Scholar 

  14. Dahn, I., Haida, A., Honigmann, T., Wernhard, C.: Using mathematica and automated theorem provers to access a mathematical library. In: Proceedings of the CADE-15 Workshop on Integration of Deductive Systems (1998)

    Google Scholar 

  15. Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The prosper toolkit. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 78. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Felty, A., Howe, D.: Hybrid interactive theorem proving using Nuprl and HOL. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 351–365. Springer, Heidelberg (1997)

    Google Scholar 

  17. Franke, A., Kohlhase, M.: MATHWEB, an agentbased communication layer for distributed automated theorem proving. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction, Trento. LNCS (LNAI), vol. 1631, pp. 217–221. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  18. Franke, A., Kohlhase, M.: MBase: representing mathematical knowledge in a relational data base. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 455–459. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  20. Hillenbrand, T., Jaeger, A., Loechner, B.: WALDMEISTER: Improvements in performance and ease of use. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 232–236. Springer, Heidelberg (1999)

    Google Scholar 

  21. Howe, D.J.: Importing mathematics from HOL in Nuprl. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 267–282. Springer, Heidelberg (1996)

    Google Scholar 

  22. Huang, X.: Human Oriented Proof Presentation: A Reconstructive Approach. PhD thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany (1994)

    Google Scholar 

  23. Huang, X.: Reconstructing Proofs at the Assertion Level. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 738–752. Springer, Heidelberg (1994)

    Google Scholar 

  24. Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: A high performance theorem prover. Journal of Automated Reasoning 8(2), 183–212 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  25. McCune, W.: OTTER 2.0. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 663–664. Springer, Heidelberg (1990)

    Google Scholar 

  26. Meier, A.: TRAMP: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 460–464. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Meier, A., Pollet, M., Sorge, V.: Classifying Isomorphic Residue Classes. In: Moreno-Díaz Jr., R., Buchberger, B., Freire, J.-L. (eds.) EUROCAST 2001. LNCS, vol. 2178, pp. 494–508. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  28. De Nivelle, H.: Bliksem 1.10 User Manual. MPI Saarbruecken (1999)

    Google Scholar 

  29. Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  30. Papakonstantinou, Y., Garcia-Molina, H., Ullman, J.: Medmaker: A mediation system based on declarative specifications. In: Proceedings of the 12th International Conference on Data Engineering, pp. 132–141. IEEE Computer Society, Los Alamitos (1996)

    Google Scholar 

  31. Riazanov, A., Voronkov, A.: VAMPIRE. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 292–296. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  32. Allen, S., Constable, R., Eaton, R., Kreitz, C., Lorigo, L.: The nuprl open logical environment. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 170–176. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  33. Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 252–266. Springer, Heidelberg (1994)

    Google Scholar 

  34. Trybulec, A., Blair, H.: Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence (IJCAI), Los Angeles, CA, USA, August 18-23, pp. 26–28. Morgan Kaufmann, San Mateo (1985)

    Google Scholar 

  35. Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Thorsten, E., Keen, E., Theobalt, C., Topic, D.: SPASS version 1.0.0. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 378–382. Springer, Heidelberg (1999)

    Google Scholar 

  36. Wiederhold, G.: Mediators in the architecture of future information systems. IEEE Computer 25(3), 38–49 (1992)

    Google Scholar 

  37. Wolfram, S.: The Mathematica Book, 4th edn. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FR 6.2 Informatik, Universität des Saarlandes, Saarbrücken, Germany

    Christoph Benzmüller & Andreas Meier

  2. School of Computer Science, University of Birmingham, UK

    Volker Sorge

Authors
  1. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Meier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Volker Sorge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter

  2. German Research Center for Artificial Intelligence, DFKI GmbH,  

    Werner Stephan

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Benzmüller, C., Meier, A., Sorge, V. (2005). Bridging Theorem Proving and Mathematical Knowledge Retrieval. In: Hutter, D., Stephan, W. (eds) Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science(), vol 2605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32254-2_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-32254-2_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25051-7

  • Online ISBN: 978-3-540-32254-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation