10 February 2015, Logic Tea, Marcos Cramer

Abstract

We have developed a controlled natural language (CNL) – i.e. a subset of a natural language defined through a formal grammar – for writing mathematical texts. The Naproche system can check the correctness of mathematical proofs written in this CNL. In this talk we will highlight some interesting logical and linguistic problems that had to be solved in the development of the Naproche CNL and the Naproche system: The system uses a formalism from the linguistic theory of presuppositions in order to work with potentially undefined terms, and can handle dynamic quantification, including the phenomenon of implicit dynamic function introduction, which had previously not been discussed in the literature. Tea and cookies will be available during the talk. Afterwards you are welcome to join for drinks in the 'Cafe Polder'.

For more information, please visit the website http://www.illc.uva.nl/logic_tea/ or contact Thomas Brochhagen (t.s.brochhagen at uva.nl), Johannes Marti (johannes.marti at gmail.com), Masa Mocnik (masa.mocnik at gmail.com) or Julian Schloder (julian.schloeder at gmail.com).