Reference : Modelling implicit dynamic introduction of function symbols in mathematical texts

Scientific congresses, symposiums and conference proceedings : Paper published in a book

Physical, chemical, mathematical & earth Sciences : Mathematics Arts & humanities : Languages & linguistics

http://hdl.handle.net/10993/20983

Modelling implicit dynamic introduction of function symbols in mathematical texts

English

Cramer, Marcos[University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]

2014

Joint Proceedings of the Second Workshop on Natural Language and Computer Science (NLCS’14) & 1st International Workshop on Natural Language Services for Reasoners (NLSR 2014) Affliated to RTA-TLCA, VSL 2014 July 17-18, 2014 Vienna, Austria.

de Paiva, Valeria

et al.

Center for Informatics and Systems of the University of Coimbra

125-135

Yes

No

International

Second Workshop on Natural Language and Computer Science (NLCS) 2014

from 17-07-2014 to 18-07-2014

[en] dynamic quantification ; Dynamic Predicate Logic ; function introduction ; language of mathematics ; formal mathematics

[en] The specialized language of mathematics has a number of linguistically and logically interesting features. One of them, which to our knowledge has not been systematically studied before, is the implicit dynamic introduction of function symbols, exemplified by constructs of the form "for every x there is an f(x) such that ...". We present an extension of Groenendijk and Stokhof's Dynamic Predicate Logic – Typed Higher-Order Dynamic Predicate Logic – which formally models this feature of the language of mathematics. Furthermore, we illustrate how the implicit dynamic introduction of function symbols is treated in the proof checking algorithm of the Naproche system.