Using and Parsing the Mizar Language
Paul A. Cairns, Jeremy Gow · Electronic Notes in Theoretical Computer Science · 2004
Mizar is a well established and successful system for producing formal mathematics. We investi- gate the acceptability of formal mathematics to mathematicians by studying the Mizar language. Specifically, we analyse various features of the Mizar language through the exercise of trying to build a grammar for it in order to parse its library. Our analysis highlights unresolved problems with the language which may have reduced its uptake by mathematicians.