The Grail theorem prover: Type theory for syntax and semantics

TL;DR

The paper introduces the Grail theorem prover, a set of tools designed for developing and testing grammars based on type-logical grammar formalism, facilitating the integration of syntax and semantics in linguistic analysis.

Contribution

It presents the Grail theorem prover as a practical tool for applying type-logical grammars to linguistic phenomena, supporting syntax-semantics interface analysis.

Findings

Supports analysis of coordination, quantifier scope, and extraction

Provides freely available tools for grammar design and testing

Enhances the application of type-logical grammars in linguistics

Abstract

As the name suggests, type-logical grammars are a grammar formalism based on logic and type theory. From the prespective of grammar design, type-logical grammars develop the syntactic and semantic aspects of linguistic phenomena hand-in-hand, letting the desired semantics of an expression inform the syntactic type and vice versa. Prototypical examples of the successful application of type-logical grammars to the syntax-semantics interface include coordination, quantifier scope and extraction.This chapter describes the Grail theorem prover, a series of tools for designing and testing grammars in various modern type-logical grammars which functions as a tool . All tools described in this chapter are freely available.