This event is from the archives of The Notice Board. The event has already taken place and the information contained in this post may no longer be relevant or accurate.
Abstract: 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.
Contact:
Barb Hodgson | hodgsonb@uleth.ca | (403) 329-2470 | uleth.ca/artsci/event/64691