Skip to main content
SpringerLink
Log in

A Query Language for Formal Mathematical Libraries

  • Conference paper
Intelligent Computer Mathematics (CICM 2012)

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

Included in the following conference series:

Abstract

One of the most promising applications of mathematical knowledge management is search: Even if we restrict attention to the tiny fragment of mathematics that has been formalized, the amount exceeds the comprehension of an individual human.

Based on the generic representation language MMT, we introduce the mathematical query language QMT: It combines simplicity, expressivity, and scalability while avoiding a commitment to a particular logical formalism. QMT can integrate various search paradigms such as unification, semantic web, or XQuery style queries, and QMT queries can span different mathematical libraries.

We have implemented QMT as a part of the MMT API. This combination provides a scalable indexing and query engine that can be readily applied to any library of mathematical knowledge. While our focus here is on libraries that are available in a content markup language, QMT naturally extends to presentation and narration markup languages.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Aspinall, D., Denney, E., Lüth, C.: Querying Proofs. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 92–106. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. ANSI/ISO/IEC. 9075:2003, Database Language SQL (2003)

    Google Scholar 

  3. Asperti, A., Selmi, M.: Efficient Retrieval of Mathematical Statements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 17–31. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Altamimi, M., Youssef, A.: A Math Query Language with an Expanded Set of Wildcards. Mathematics in Computer Science 2, 305–331 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  5. Buswell, S., Caprotti, O., Carlisle, D., Dewar, M., Gaetano, M., Kohlhase, M.: The Open Math Standard, Version 2.0. Technical report. The Open Math Society (2004), http://www.openmath.org/standard/om20

  6. Bancerek, G., Rudnicki, P.: Information Retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 119–132. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project Abstract: Logic Atlas and Integrator (LATIN). In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS, vol. 6824, pp. 289–291. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Guidi, F., Sacerdoti Coen, C.: Querying Distributed Digital Libraries of Mathematics. In: Hardin, T., Rioboo, R. (eds.) Proceedings of Calculemus, pp. 17–30 (2003)

    Google Scholar 

  9. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  10. Kohlhase, M.: OMDoc – An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol. 4180. Springer, Heidelberg (2006)

    Book  Google Scholar 

  11. Kohlhase, M., Rabe, F., Zholudev, V.: Towards MKM in the Large: Modular Representation and Scalable Software Architecture. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P., Rideau, L., Rioboo, R., Sexton, A. (eds.) AISC 2010. LNCS, vol. 6167, pp. 370–384. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Kohlhase, M., Sucan, I.: A Search Engine for Mathematical Formulae. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 241–253. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Libbrecht, P., Melis, E.: Methods to Access and Retrieve Mathematical Content in ActiveMath. In: Iglesias, A., Takayama, N. (eds.) ICMS 2006. LNCS, vol. 4151, pp. 331–342. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Mišutka, J., Galamboš, L.: Extending full text search engine for mathematical content. In: Sojka, P. (ed.) Towards a Digital Mathematics Lbrary, pp. 55–67 (2008)

    Google Scholar 

  15. Munavalli, R., Miner, R.: MathFind: a math-aware search engine. In: Efthimiadis, E., Dumais, S., Hawking, D., Järvelin, K. (eds.) International ACM SIGIR Conference on Research and Development in Information Retrieval, p. 735. ACM (2006)

    Google Scholar 

  16. Miller, B., Youssef, A.: Technical Aspects of the Digital Library of Mathematical Functions. Annals of Mathematics and Artificial Intelligence 38(1-3), 121–136 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  17. Rabe, F.: The MMT System (2008), https://trac.kwarc.info/MMT/

  18. Rabe, F., Kohlhase, M.: A Scalable Module System (2011), http://arxiv.org/abs/1105.0548

  19. Sojka, P., Líška, M.: Indexing and Searching Mathematics in Digital Libraries - Architecture, Design and Scalability Issues. In: Davenport, J., Farmer, W., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS, vol. 6824, pp. 228–243. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  21. Trybulec, A., Blair, H.: Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26–28 (1985)

    Google Scholar 

  22. Urban, J.: MOMM - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. International Journal on Artificial Intelligence Tools 15(1), 109–130 (2006)

    Article  Google Scholar 

  23. W3C. Mathematical Markup Language (MathML) Version 2.0., 2nd edn. (2003), http://www.w3.org/TR/MathML2

  24. W3C. XQuery 1.0: An XML Query Language (2007), http://www.w3.org/TR/xquery/

  25. W3C. SPARQL Query Language for RDF (2008), http://www.w3.org/TR/rdf-sparql-query/

  26. Zholudev, V., Kohlhase, M.: TNTBase: a Versioned Storage for XML. In: Proceedings of Balisage: The Markup Conference 2009. Balisage Series on Markup Technologies, vol. 3, Mulberry Technologies, Inc. (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Jacobs University Bremen, Germany

    Florian Rabe

Authors
  1. Florian Rabe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information and Computing Sciences, Utrecht University and Open Universiteit Nederland, Princetonplein 5, 3584 CC, Utrecht, The Netherlands

    Johan Jeuring

  2. Department of Computer Science, University College London, Gower Street, WC1E 6BT, London, UK

    John A. Campbell

  3. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, ON, Canada

    Jacques Carette

  4. Department of Computer Science and Engineering, Texas A&M University, 77843-3112, College Station, TX, USA

    Gabriel Dos Reis

  5. Department of Computer Graphics and Design, Masaryk University, Botanická 68a, 60200, Brno, Czech Republic

    Petr Sojka

  6. Laboratoire de Recherche en Informatique (LRI - UMR8623) PCRI, Université Paris-Sud, Batiment 650, 91405, Orsay Cedex, France

    Makarius Wenzel

  7. The University of Birmingham, School of Computer Science,, B15 2TT, Edgbaston, Birmingham, UK

    Volker Sorge

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rabe, F. (2012). A Query Language for Formal Mathematical Libraries. In: Jeuring, J., et al. Intelligent Computer Mathematics. CICM 2012. Lecture Notes in Computer Science(), vol 7362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31374-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31374-5_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31373-8

  • Online ISBN: 978-3-642-31374-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation