skip to content

Interest Group in Formal Mathematics: Natural Language Proof Checking - The Naproche System

Presented by: 
M Cramer & P Koepke & B Schroeder [Universities of Bonn and Duisburg/Essen]
Wednesday 28th March 2012 - 14:00 to 16:00
INI Discussion Room
We shall present the Naproche Proof Checking System which accepts mathematical text formulated in a controlled natural language close to the mathematical vernacular. The project involves work on several levels: linguistics for processing the input language, logic for providing natural proof methods, and mathematics for the formalization process and background theories. We shall shall discuss some "natural" example texts acceptable by the System.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons