Skip to Main content Skip to Navigation
Book sections

The Grail Theorem Prover: Type Theory for Syntax and Semantics

Richard Moot 1, 2
1 TEXTE - Exploration et exploitation de données textuelles
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
Abstract : Type-logical grammars use a foundation of logic and type theory to model natural language. These grammars have been particularly successful giving an account of several well-known phenomena on the syntax-semantics interface, such as quantifier scope and its interaction with other phenomena. This chapter gives a high-level description of a family of theorem provers designed for grammar development in a variety of modern type-logical grammars. We discuss automated theorem proving for type-logical grammars from the perspective of proof nets, a graph-theoretic way to represent (partial) proofs during proof search.
Document type :
Book sections
Complete list of metadata
Contributor : Richard Moot <>
Submitted on : Monday, February 20, 2017 - 11:06:23 AM
Last modification on : Friday, June 4, 2021 - 12:32:02 PM
Long-term archiving on: : Sunday, May 21, 2017 - 1:12:58 PM


chapter (1).pdf
Files produced by the author(s)



Richard Moot. The Grail Theorem Prover: Type Theory for Syntax and Semantics. Zhaohui Luo; Stergios Chatzikyriakidis. Modern Perspectives in Type-Theoretical Semantics, Studies in Linguistics and Philosophy (98), Springer, pp.247-277, 2017, Part III, 978-3-319-50420-9. ⟨10.1007/978-3-319-50422-3_10⟩. ⟨lirmm-01471644⟩



Record views


Files downloads