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

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.

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)