PIMS-ULethbridge PIMS Distinguished Visitor Series: Fairouz Kamareddine

  • Date: 02/05/2015
  • Time: 12:15
Lecturer(s):
 Fairouz Kamareddine, Heriot-Watt University
Location: 

University of Lethbridge

Topic: 

Computerising Mathematical Texts with MathLang

Description: 

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