Skip to main content
Contribution to Book
Proof Tree Automata
Words, Proofs, and Diagrams (2002)
  • Hans Joerg Tiede, Illinois Wesleyan University

In this paper, we continue our investigation of the strong generative capacity of proof theoretical grammars using natural deduction proof trees as the structures that grammars assign to their languages. We review the results that were previously obtained for associative Lambek grammars and extend the methods used there to non-associative Lambek grammars. The main result of this paper is that non-associative Lambek grammars, which generate precisely the context-free string languages, can assign structures to their languages that are not local, thus more complex than the structures context-free grammars can assign. When only proof trees in normal form are considered, the tree languages assigned by non-associative Lambek grammars are always regular, thus their structures are less complex than those of associative Lambek grammars, which have been shown to be able to assign non-regular tree languages to their languages. As AB grammars (also known as categorial grammars) only assign local tree languages to their languages, we arrive at a hierarchy of proof theoretical grammars with respect to their strong generative capacity.

Publication Date
Dave Barker-Plummer, David I. Beaver, Johan van Benthem, and Patrick Scotto di Luzio
CSLI Publications
Citation Information
Hans Joerg Tiede. "Proof Tree Automata" Words, Proofs, and Diagrams (2002)
Available at: