In this paper we propose a way to deal with natural language inference by implementing Modern Type Theoretical Semantics in the proof assistant Coq. The paper is a first attempt to deal with NLI and natural language reasoning in general by using the proof assistant technology. Valid NLIs are treated as theorems and as such the adequacy of our account is tested by trying to prove them. We use Luo’s Modern Type Theory with coercive subtyping as the formal language into which we translate natural language semantics, and we further implement these semantics in the Coq proof assistant. It is shown that the use of a MTT with an adequate subtyping mechanism can give us a number of promising results as regards NLI. Specifically, it is shown that a number of inference cases, i.e. quantifiers, adjectives, conjoined noun phrases and temporal reference among other things can be successfully dealt with. It is then shown, that even though Coq is an interactive and not an automated theorem prover, automation of all of the test examples is possible by introducing user-defined automated tactics. Lastly, the paper offers a number of innovative approaches to NL phenomena like adjectives, collective predication, comparatives and factive verbs among other things, contributing in this respect to the theoretical study of formal semantics using MTTs.
Keywords Type theory  Coercive subtyping  Natural language inference  Formal semantics  Coq  FraCas test suite
Categories (categorize this paper)
DOI 10.1007/s10849-014-9208-x
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 60,992
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Logical Form of Action Sentences.Donald Davidson - 1967 - In Nicholas Rescher (ed.), The Logic of Decision and Action. University of Pittsburgh Press. pp. 81--95.
The Proper Treatment of Quantification in Ordinary English.Richard Montague - 1973 - In Patrick Suppes, Julius Moravcsik & Jaakko Hintikka (eds.), Approaches to Natural Language. Dordrecht. pp. 221--242.
Formal Philosophy. [REVIEW]Richard Montague - 1975 - Canadian Journal of Philosophy 4 (3):573-578.

View all 21 references / Add more references

Citations of this work BETA

Natural Language Semantics and Computability.Richard Moot & Christian Retoré - 2019 - Journal of Logic, Language and Information 28 (2):287-307.

Add more citations

Similar books and articles

Formal Semantics in Modern Type Theories with Coercive Subtyping.Zhaohui Luo - 2012 - Linguistics and Philosophy 35 (6):491-513.
An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics.Chris Fox & Shalom Lappin - 2004 - Logic Journal of the Interest Group in Pure and Applied Logics 12 (2):135--168.
Formal Semantics in the Age of Pragmatics.Juan Barba - 2007 - Linguistics and Philosophy 30 (6):637-668.
Fragments of Language.Ian Pratt-Hartmann - 2004 - Journal of Logic, Language and Information 13 (2):207-223.
On What Actually Is.Fredrik Haraldsen - 2015 - Erkenntnis 80 (3):643-656.


Added to PP index

Total views
63 ( #165,284 of 2,439,431 )

Recent downloads (6 months)
3 ( #209,215 of 2,439,431 )

How can I increase my downloads?


My notes