PIMS-ULethbridge PIMS Distinguished Visitor Series: Fairouz Kamareddine

  • Date: 02/05/2015
  • Time: 12:15
 Fairouz Kamareddine, Heriot-Watt University

University of Lethbridge


Computerising Mathematical Texts with MathLang


Mathematical texts can be computerised in many ways. At one end there is document imaging, at the other there are proof assistants (Mizar, Isabelle, Coq, etc.).In between, there are typesetting (e.g., LaTeX and MathML) and semantically oriented (e.g., OpenMath and OMDoc) systems. MathLang is an approach for computerising mathematical texts which is flexible enough to connect the different approaches to computerisation, allowing various degrees of formalisation and compatibility with different logical frameworks (set/cate­gory/type theory) and proof systems.


MathLang adds, checks, and displays various information aspects on mathematical texts. One aspect is a weak type system that assigns categories (term, statement, noun, adjective, etc.) to parts of the text, and checks that grammatical sense is maintained. Another aspect allows identifying chunks of text, marking their roles (theorem, definition, explanation, example, section, etc.), and indicating relation­ships between the chunks (A contradicts B, A follows from B, etc.). Further aspects allow additional formality such as proof structure and details of how a human-readable proof is encoded into a fully formalised version of Mizar/Isabelle/Coq. In this talk we survey the status of the MathLang project.


Other Information: 

Location: B730, University Hall, University of Lethbridge


Don’t miss Professor Kamareddine’s first talk on Monday February 2nd:
Types and Functions Since Principia and Computerisation of Language and Mathematics


Learn more at uleth.ca/artsci/event/64690