An extensible proof text editor

Abstract

The paper presents an extension of the proof editor Alfa with natural-language input and output. The basis of the new functionality is an automatic translation to syntactic structures that are closer to natural language than the type-theoretical syntax of Alfa. These syntactic structures are mapped into texts in languages such as English, French, and Swedish. In this way, every theory, definition, proposition, and proof in Alfa can be translated into a text in any of these languages. The translation is defined for incomplete proof objects as well, so that a text with “holes” (i.e. metavariables) in it can be viewed simultaneously with a formal proof constructed. The mappings into natural language also work in the parsing direction, so that input can be given to the proof editor in a natural language. The natural-language interface is implemented using the Grammatical Framework GF, so that it is possible to change and extend the interface without recompiling the proof editor. Such extensions can be made on two dimensions: by adding new target languages, and by adding theoryspecific grammatical annotations to make texts more idiomatic.