The Naproche project (Natural language Proof Checking) studies the semi-formal language of mathematics from a linguistic, philosophical and mathematical perspective. A central goal of Naproche is to develop a controlled natural language (CNL) for mathematical texts and adapted proof checking software which checks texts written in the CNL for syntactical and mathematical correctness. The Naproche system is an implementation of the ideas developed by the Naproche project. It accepts a controlled but rich subset of ordinary mathematical language including TeX-style typeset formulas and transforms them into formal statements. Linguistic techniques are adapted to allow for common grammatical constructs and to extract mathematically relevant implicit information about hypotheses and conclusions. Finally, automated theorem provers are used to prove the correctness of the input text.
Keywords for this software
References in zbMATH (referenced in 12 articles , 1 standard article )
Showing results 1 to 12 of 12.
- De Lon, Adrian; Koepke, Peter; Lorenzen, Anton: Interpreting mathematical texts in Naproche-SAD (2020)
- Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; Pease, Alison: Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues (2017)
- Ganesalingam, M.; Gowers, W. T.: A fully automatic theorem prover with human-style output (2017)
- Pease, Alison; Lawrence, John; Budzynska, Katarzyna; Corneli, Joseph; Reed, Chris: Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation (2017)
- Youssef, Abdou: Part-of-math tagging and applications (2017)
- Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
- Leiß, Hans; Wu, Shuqian: Type reconstruction for (\lambda)-DRT applied to pronoun resolution (2016)
- Cramer, Marcos; Schröder, Bernhard: Interpreting plurals in the naproche CNL (2012) ioport
- Cramer, Marcos; Koepke, Peter; Schröder, Bernhard: Parsing and disambiguation of symbolic mathematics in the Naproche system (2011)
- Ranta, Aarne: Translating between language and logic: what is easy and what is difficult (2011)
- Cramer, Marcos; Fisseni, Bernhard; Koepke, Peter; Kühlwein, Daniel; Schröder, Bernhard; Veldman, Jip: The Naproche project controlled natural language proof checking of mathematical texts (2010) ioport
- Cramer, Marcos; Koepke, Peter; Kühlwein, Daniel; Schröder, Bernhard: Premise selection in the Naproche system (2010)