MITACS Seminar Series on Mathematics of Computer Algebra and Analysis

A Language for Mathematical Knowledge Management.

Steven Keiffer, Mathematics, SFU

3:30pm, Friday March 7th, 2008, in IRMACS 10908.

Abstract: 

With the growing use of digital means of storing, communicating,
accessing, and manipulating mathematical knowledge, it becomes
important to develop appropriate formal languages for the
representation of such knowledge. But the scope of  ``mathematical
knowledge'' is broad, and the meaning of the word  ``appropriate'' will
vary from application to application. At the  extremes, there are
competing desiderata:  At the foundational level, one wants a small and
simple  syntax, and a precise specification of its semantics. In
particular,  one wants a specification as to which inferences are
valid.  At the human level, one wants to have mathematical  languages
that are as easy to read and understand as ordinary  mathematical texts,
yet also admit a precise interpretation to the  foundational level.

Our main goal here is to show that the distance between the
foundational level and ordinary mathematical text is not as far as is
commonly supposed, by presenting a syntactically sugared version of  set
theory that is simultaneously close to both. We show that, on the one
hand, our language is easily parsed and translated to the language of
set theory; on the other hand, by automatically replacing symbolic
expressions with user-provided natural-language equivalents, we obtain
output that is humanly readable, and, although not exactly literary,
recognizably faithful to the original mathematical texts.