Proof Assistants for Natural Language Semantics

Stergios Chatzikyriakidis, Zhaohui Luo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

73 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationLogical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996–2016)
Subtitle of host publication9th International Conference, LACL 2016, Nancy, France, December 5-7, 2016, Proceedings
PublisherSpringer Heidelberg
Number of pages14
ISBN (Electronic)978-3-662-53826-5
ISBN (Print)978-3-662-53825-8
Publication statusE-pub ahead of print - 10 Nov 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Cite this