A Language for Mathematical Knowledge Management
Steven Kieffer, Mathematics, SFU.
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.