TY - CHAP

T1 - Flexible encoding of mathematics on the computer

AU - Kamareddine, Fairouz

AU - Maarek, Manuel

AU - Wells, J. B.

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33745641592&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-27818-4_12

DO - 10.1007/978-3-540-27818-4_12

M3 - Chapter (peer-reviewed)

SN - 978-3-540-23029-8

VL - 3119

T3 - Lecture Notes in Computer Science

SP - 160

EP - 174

BT - Mathematical Knowledge Management

T2 - Third International Conference on Mathematical Knowledge Management

Y2 - 19 September 2004 through 21 September 2004

ER -