Semantic representation of mathematics
Or, knowledge representation for mathematics. Applications include proof assistants and automated theorem provers. Related to the foundations of mathematics.
Community activity
- 2016 Fields Institute Workshop on Semantic Representation of Mathematical
Knowledge :
- Documentary-style summary video and talks
- Good talks by
- Jeremy Avigad (slides 1 ,2 ), a developer of the Lean theorem prover
- Sessions at ICMS 2018 (doi):
- Session 8 : Machine learning for mathematical software
- Session 19 : Formal and informal mathematical corpora
Projects
Standards
- Mathematical Markup Language (MathML)
- Two flavors: Presentation and Content
- Hodson, 2014: Ry’s MathML Tutorial (epub ) (only Presentation MathML)
- Barnhart: Connexions Guide to MathML, Sec 3: Content MathML (epub )
- OpenMath
- Technical overview
- Comparison with MathML
- MathML is for presentation, OpenMath is for semantics
- For high-school level math, both Content MathML and OpenMath work
- For more advanced math, only OpenMath defines semantics
- Dalmas et al, 1997: An OpenMath 1.0 Implementation (doi, pdf)
- Buswell et al, 2004: The OpenMath 2.0 Standard (pdf)
- OMDoc : Open Mathematical Documents
- Container for MathML and OpenMath
- Extends OpenMath from expressions to also statements and theories
- Kohlhase, 2006: /OMDoc 1.2 Book /(pdf)
Libraries
MO has a big list of “atlas-like websites” for specific areas of mathematics.
- Digital Library of Mathematical Functions (DLMF)
- Miller & Youssef, 2003: Technical aspects of the DLMF (doi)
- Digital Repository of Mathematical Formulae (DRMF)
- Global Digital Mathematics Library (GDML)
- Mathematical Functions Grimoire (FunGrim) (GitHub )
- Similar in scope to DLMF but fully open and greater emphasis on semantics
- Johansson, 2020: FunGrim: a symbolic library for special functions (arxiv)
Literature
General
- Carette, Farmer, Kohlhase, Rabe, 2019: Big math and the one-brain barrier: A position paper and architecture proposal (arxiv)
Semantic Web
- Lange, 2013: Ontologies and languages for representing mathematical knowledge on the Semantic Web (doi, pdf)
- Bröcheler, 2007: A mathematical semantic web (pdf)
Recognizing and parsing mathematical expressions
- Zanibbi & Blostein, 2012: Recognition and retrieval of mathematical expressions (doi)
- Chan & Yeung, 2000: Mathematical expression recognition: a survey (doi)
Parsing LaTeX:
- Chien & Cheng, 2015: Semantic tagging of mathematical expressions (doi, pdf)
- Fateman & Capsi, 1999: Parsing TeX into mathematics (pdf)
Parsing PostScript and PDF:
- Yang & Fateman, 2003: Extracting mathematical expressions from PS documents (pdf)