To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Proof Assistants for Natu… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Proof Assistants for Natural Language Semantics

Conference paper
Authors Stergios Chatzikyriakidis
Zhaohui Luo
Published in Logical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996–2016) 9th International Conference, LACL 2016, Nancy, France, December 5-7, 2016, Proceedings / edited by Maxime Amblard, Philippe de Groote, Sylvain Pogodalla, Christian Retoré.
ISBN 978-3-662-53825-8
ISSN 0302-9743
Publisher Berlin Heidelberg
Place of publication Springer
Publication year 2016
Published at Department of Philosophy, Linguistics and Theory of Science
Language en
Subject categories Languages and Literature, Computer and Information Science


In this paper we discuss the use of interactive theorem provers (also called proof assistants) in the study of natural language semantics. It is shown that these provide useful platforms for NL semantics and reasoning on the one hand, and allow experiments to be performed on various frameworks and new theories, on the other. In particular, we show how to use Coq, a prominent type theory based proof assistant, to encode type theoretical semantics of various NL phenomena. In this respect, we can encode the NL semantics based on type theory for quantifiers, adjectives, common nouns, and tense, among others, and it is shown that Coq is a powerful engine for checking the formal validity of these accounts as well as a powerful reasoner about the implemented semantics. We further show some toy semantic grammars for formal semantic systems, like the Montagovian Generative Lexicon, Type Theory with Records and neo-Davidsonian semantics. It is also explained that experiments on new theories can be done as well, testing their validity and usefulness. Our aim is to show the importance of using proof assistants as useful tools in natural language reasoning and verification and argue for their wider application in the field.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?