An Extensible Proof Text Editor
An Extensible Proof Text Editor
复制标题
可扩展的校样文本编辑器
DOI：
10.1007/3-540-44404-1_6
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
Aarne Ranta
中科院分区：
文献类型：
--
作者：
T. Hallgren;Aarne Ranta
本文提出了一种具有自然语言输入和输出功能的校对编辑器ALFA的扩展。新功能的基础是自动转换为比Alfa的类型理论语法更接近自然语言的句法结构。这些句法结构被映射到英语、法语和瑞典语等语言的文本中。通过这种方式，阿尔法中的每个理论、定义、命题和证明都可以被翻译成这些语言中的任何一种文本。翻译也是为不完整的证明对象定义的，以便在构造正式证明的同时，可以查看其中有“洞”(即，元变量)的文本。到自然语言的映射也在分析方向上工作，因此可以用自然语言向校对编辑提供输入。
自然语言接口是使用语法框架GF实现的，因此可以在不重新编译校对编辑器的情况下改变和扩展接口。这样的扩展可以从两个方面进行：通过增加新的目标语言，以及通过增加特定于理论的语法注释，使文本更加地道。
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.