The Grail Theorem Prover: Type Theory for Syntax and Semantics

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.