The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts

被引：0

作者：

Cramer, Marcos ^{[1
,2
]}

Fisseni, Bernhard ^{[1
,2
]}

Koepke, Peter ^{[1
,2
]}

Kuehlwein, Daniel ^{[1
,2
]}

Schroeder, Bernhard ^{[1
,2
]}

Veldman, Jip ^{[1
,2
]}

机构：

[1] Univ Bonn, D-5300 Bonn, Germany

[2] Univ Duisburg, D-47057 Duisburg, Germany

来源：

CONTROLLED NATURAL LANGUAGE | 2010年 / 5972卷

关键词：

CNL; mathematical language; formal mathematics; proof checking;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper discusses the semi-formal language of mathematics and presents the Naproche CNL, a controlled natural language for mathematical authoring. Proof Representation Structures, an adaptation of Discourse Representation Structures, are used to represent the semantics of texts written in the Naproche CNL. We discuss how the Naproche CNL can be used in formal mathematics, and present our prototypical Naproche system, a computer program for parsing texts in the Naproche CNL and checking the proofs in them for logical correctness.

引用

页码：170 / +

页数：2