Sciweavers

MKM
2005
Springer

Translating Mathematical Vernacular into Knowledge Repositories

13 years 9 months ago
Translating Mathematical Vernacular into Knowledge Repositories
Abstract. Defining functions is a major topic when building mathematical repositories. Though relatively easy in mathematical vernacular, function definitions rise a number of questions and problems in fully formal languages (see [Dav03]). This becomes even more important for repositories in which properties of the defined functions are not only stated, but also proved correct. In this paper we investigate function definitions in the Mizar system. Though most of them are straightforward and follow the intuition, we also found a number of examples differing from mathematical vernacular or where different solutions seem equally reasonable. Sometimes there even do not seem to exist solutions not somehow “ignoring mathematical vernacular”. So the question is: Should we seek for some kind of standard, that is a “formal mathematical vernacular”, or should we accept that different authors prefer different styles?
Adam Grabowski, Christoph Schwarzweller
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where MKM
Authors Adam Grabowski, Christoph Schwarzweller
Comments (0)