## PIMS-ULethbridge PIMS Distinguished Visitor Series: Fairouz Kamareddine

- Date: 02/05/2015
- Time: 12:15

*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/category/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 relationships 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.

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