Title: An Extensible Proof Text Editor
Authors: Thomas Hallgren, Aarne Ranta
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
theory-specific grammatical annotations to make texts more
idiomatic.