Skip to main content
SpringerLink
Log in

Formalized Mathematical Content in Lecture Notes on Modelling and Analysis

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2018)

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

Included in the following conference series:

  • 618 Accesses

Abstract

We introduce an approach to include formalized mathematics in regular undergraduate mathematics courses. In order to enable automatic parsing and checking, the code of our lecture notes systematically uses strict syntax conventions for all definitions and theorems, including in particular an unambiguous grammar for all formulas. Resulting from several years of experience, we present a body of about 1000 pages of notes for a course on modelling and a sequence of three courses on analysis and calculus which are a regular part in the undergraduate mathematics curriculum at the University of Constance. We explain the basic structure of the formalization and its syntax and discuss the practicability of the approach.

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 EPUB and 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

References

  1. MMATh-Homepage: Currently in German: http://www.math.uni-konstanz.de/mmath

  2. LaTeX-Sources: LATEX and PDF versions of the analysis lecture notes (in German). http://www.math.uni-konstanz.de/mmath/download

  3. Kohlhase, M.: Using LaTeX as a semantic markup format. Math. Comput. Sci. 2, 279–304 (2008)

    Article  Google Scholar 

  4. Mizar-Homepage. http://www.mizar.org/

  5. Knuth, D.E.: Literate Programming. Comput. J. 27(2), 97–111 (1984)

    Article  Google Scholar 

  6. Kohlhase, M.: OMDoc - An Open Markup Format for Mathematical Documents [version 1.2]. Springer, Heidelberg (2006). https://doi.org/10.1007/11826095

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität Konstanz, Fach D194, 78457, Konstanz, Germany

    Michael Junk, Stefan Hölle & Sebastian Sahli

Authors
  1. Michael Junk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Hölle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sebastian Sahli
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Junk .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Bayern, Germany

    Florian Rabe

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    William M. Farmer

  3. University of Cambridge, Cambridge, United Kingdom

    Grant O. Passmore

  4. Department of Computer Science, The George Washington University, Washington, District of Columbia, USA

    Abdou Youssef

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Junk, M., Hölle, S., Sahli, S. (2018). Formalized Mathematical Content in Lecture Notes on Modelling and Analysis. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-96812-4_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-96811-7

  • Online ISBN: 978-3-319-96812-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation