Proof Assistants for Natural Language Semantics

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.