Skip to main content
Springer Nature Link
Log in

Parsing and Disambiguation of Symbolic Mathematics in the Naproche System

  • Conference paper
Intelligent Computer Mathematics (CICM 2011)

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

Included in the following conference series:

  • 661 Accesses

Abstract

The Naproche system is a system for linguistically analysing and proof-checking mathematical texts written in a controlled natural language. The aim is to have an input language that is as close as possible to the language that mathematicians actually use when writing textbooks or papers.

Mathematical texts consist of a combination of natural language and symbolic mathematics, with symbolic mathematics obeying its own syntactic rules. We discuss the difficulties that a program for parsing and disambiguating symbolic mathematics must face and present how these difficulties have been tackled in the Naproche system. One of these difficulties is the fact that information provided in the preceding context – including information provided in natural language – can influence the way a symbolic expression has to be disambiguated.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 52.74
Price includes VAT (France)
  • 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.

Similar content being viewed by others

References

  1. Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic 9(1:2) (2007)

    Google Scholar 

  2. Brachman, R., Levesque, H.: Knowledge Representation and Reasoning. Morgan Kaufmann Publishers, Massachusetts (2004)

    MATH  Google Scholar 

  3. de Bruijn, R.G.: Reflections on Automath. In: Nederpelt, R.P., et al. (eds.) Selected Papers on Automath. Studies in Logic, vol. 133, pp. 201–228, 215. Elsevier, Amsterdam (1994)

    Chapter  Google Scholar 

  4. Carl, M., Cramer, M., Kühlwein, D.: Chapter 1 from Landau in Naproche 0.5 (2011), http://naproche.net/downloads/2011/landauChapter1.pdf

  5. Church, A.: A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic 5(2), 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  6. Cramer, M., Koepke, P., Kühlwein, D., Schröder, B.: The Naproche System. Calculemus, Emerging Trend Paper (2009)

    Google Scholar 

  7. Cramer, M., Fisseni, B., Koepke, P., Kühlwein, D., Schröder, B., Veldman, J.: The Naproche Project – Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, N.E. (ed.) CNL 2009. LNCS, vol. 5972, pp. 170–186. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Cramer, M., Kühlwein, D., Schröder, B.: Presupposition Projection and Accommodation in Mathematical Texts. In: Semantic Approaches in Natural Language Processing: Proceedings of the Conference on Natural Language Processing 2010 (KONVENS), pp. 29–36. Universaar (2010)

    Google Scholar 

  9. Ganesalingam, M.: The Language of Mathematics, PhD thesis, University of Cambridge (2009)

    Google Scholar 

  10. Hales, T.: Jordan’s proof of the Jordan Curve theorem. Studies in Logic, Grammar and Rhetoric 10(23) (2007)

    Google Scholar 

  11. Hales, T.: Introduction to the Flyspeck Project. Dagstuhl Seminar Proceedings (2006)

    Google Scholar 

  12. Heuser, H.: Lehrbuch der Analysis. In: Teil 2, 6th edn., B.G. Teubner, Stuttgart (1991)

    Google Scholar 

  13. Kadmon, N.: Formal Pragmatics. Wiley-Blackwell, Oxford, UK (2001)

    Google Scholar 

  14. Kamp, H., Reyle, U.: From Discourse to Logic: Introduction to Model-theoretic Semantics of Natural Language. Kluwer Academic Publishers, Dordrecht (1993)

    Google Scholar 

  15. Lackenby, M.: Topology and Groups. Lecture Notes (2008), http://people.maths.ox.ac.uk/lackenby/tg050908.pdf

  16. Landau, E.: Grundlagen der Analysis, 3rd edn (1960)

    Google Scholar 

  17. Matuszewski, R., Rudnicki, P.: Mizar: The first 30 years. Mechanized Mathematics and Its Applications 4 (2005)

    Google Scholar 

  18. Ranta, A.: Structure grammaticales dans le français mathématique II (suite et fin). Mathématiques, Informatique et Sciences Humaines 139, 5–36 (1997)

    MathSciNet  Google Scholar 

  19. Verchinine, K., Lyaletski, A., Paskevich, A.: System for Automated Deduction (SAD): a tool for proof verification. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 398–403. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bonn, Germany

    Marcos Cramer, Peter Koepke & Bernhard Schröder

  2. University of Duisburg-Essen, Germany

    Marcos Cramer, Peter Koepke & Bernhard Schröder

Authors
  1. Marcos Cramer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Koepke
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bernhard Schröder
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departments of Computer Science and Mathematics Sciences, University of Bath, BA2 7AY, United Kingdom

    James H. Davenport

  2. Department of Computing and Software, McMaster University, 1280 Main Street West, L8SK1, Hamilton, Ontario, Canada

    William M. Farmer

  3. Institute for Computing and Information Sciences, Radboud University, Heyendaalseweg 135, 6525 AJ, Nijmegen, The Netherlands

    Josef Urban

  4. Department of Computer Science, Jacobs University Bremen, Campus Ring 12, 28759, Bremen, Germany

    Florian Rabe

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cramer, M., Koepke, P., Schröder, B. (2011). Parsing and Disambiguation of Symbolic Mathematics in the Naproche System. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds) Intelligent Computer Mathematics. CICM 2011. Lecture Notes in Computer Science(), vol 6824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22673-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22673-1_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22672-4

  • Online ISBN: 978-3-642-22673-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation