Type-Logical Grammar Theorem Prover

The Theorem Prover

This site is devoted to the:

This theorem prover provides a parser for type-logical grammar, a variety of categorial grammar.

Technical Background

The Prolog parser is based on a bottom-up chart parser for phrase structure grammars. Empty categories are handled as usual, and hypotheticals are assumed where specified in the input, and then discharged by a Cooper-storage-like mechanism. Each rule checks that the tree that it has created is normal. The terms are displayed in beta-eta-normal form. You can check out:

There is a separate document explaining the:


This theorem prover was used to generate the examples in Bob Carpenter's book, Type-Logical Semantics (1998, MIT Press).

In early 2000, the web server at CMU with my CGI was retired after about five years of continuous service.

In October 2000, Geert Kloosterman, of the University of Groningen in the Netherlands, reimplimented the CGI handler on their local server, which is where results are currently being served from.

Directory:     TLG Home   |   Help   |   Parser   |   Lexicon

Copyright ©1999-2000. All rights reserved.   Contact: webmaster@colloquial.com   Updated:   2 October 2000