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 metadatas

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01471644
Contributor : Richard Moot <>
Submitted on : Monday, February 20, 2017 - 11:06:23 AM
Last modification on : Thursday, May 16, 2019 - 8:22:01 PM
Long-term archiving on: Sunday, May 21, 2017 - 1:12:58 PM

Files

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

Identifiers

Citation

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⟩

Share

Metrics

Record views

319

Files downloads

1085