The Naproche Project. Controlled Natural Language Proof Checking of Mathematical Texts
- 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.
Author: | Marcos CramerGND, Bernhard FisseniGND, Peter Koepke, Daniel KühlweinGND, Bernhard SchröderGND, Jip Veldman |
---|---|
URN: | urn:nbn:de:bsz:mh39-81935 |
DOI: | https://doi.org/10.1007/978-3-642-14418-9_11 |
ISBN: | 978-3-642-14418-9 |
Parent Title (English): | Controlled Natural Language. Workshop on Controlled Natural Language, CNL 2009, Marettimo Island, Italy, June 8-10, 2009. Revised Papers |
Series (Serial Number): | Lecture Notes in Computer Science (5972) |
Publisher: | Springer |
Place of publication: | Berlin [u.a.] |
Editor: | Norbert E. Fuchs |
Document Type: | Conference Proceeding |
Language: | English |
Year of first Publication: | 2010 |
Date of Publication (online): | 2018/11/05 |
Publicationstate: | Postprint |
Reviewstate: | (Verlags)-Lektorat |
Tag: | CNL; formal mathematics; mathematical language; proof checking |
GND Keyword: | Automatisches Beweisverfahren; Computerlinguistik; Formale Semantik; Natürliche Sprache; Texttechnologie |
First Page: | 170 |
Last Page: | 186 |
DDC classes: | 400 Sprache / 400 Sprache, Linguistik |
Open Access?: | ja |
Linguistics-Classification: | Computerlinguistik |
Licence (German): | Urheberrechtlich geschützt |