Flexible encoding of mathematics on the computer

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

5 Citations (Scopus)

Abstract

This paper reports on refinements and extensions to the MathLang framework that add substantial support for natural language text. We show how the extended framework supports multiple views of mathematical texts, including natural language views using the exact text that the mathematician wants to use. Thus, MathLang now supports the ability to capture the essential mathematical structure of mathematics written using natural language text. We show examples of how arbitrary mathematical text can be encoded in MathLang without needing to change any of the words or symbols of the texts or their order. In particular, we show the encoding of a theorem and its proof that has been used by Wiedijk for comparing many theorem prover representations of mathematics, namely the irrationality of v2 (originally due to Pythagoras). We encode a 1960 version by Hardy and Wright, and a more recent version by Barendregt. © Springer-Verlag Berlin Heidelberg 2004.

Original languageEnglish
Title of host publicationMathematical Knowledge Management
Subtitle of host publicationThird International Conference, MKM 2004, Białowieża, Poland, September 19-21, 2004. Proceedings
Pages160-174
Number of pages15
Volume3119
ISBN (Electronic)978-3-540-27818-4
DOIs
Publication statusPublished - 2004
EventThird International Conference on Mathematical Knowledge Management - Białowieża, Poland
Duration: 19 Sep 200421 Sep 2004

Publication series

NameLecture Notes in Computer Science
Volume3119
ISSN (Print)0302-9743

Conference

ConferenceThird International Conference on Mathematical Knowledge Management
Abbreviated titleMKM 2004
CountryPoland
CityBiałowieża
Period19/09/0421/09/04

Cite this