A Language for Mathematical Knowledge Management

Steven Kieffer, Mathematics, SFU.

Friday March 7th, 2008 at 3:30pm in the 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.