Paper: Proof Figures And Structural Operators For Categorial Grammar

ACL ID E91-1035
Title Proof Figures And Structural Operators For Categorial Grammar
Venue Annual Meeting of The European Chapter of The Association of Computational Linguistics
Session Main Conference
Year 1991
Authors

Use of Lambek's (1958) categorial grammar for lin- guistic work has generally been rather limited. There appear to be two main reasons for this: the nota- tions most commonly used can sometimes obscure the structure of proofs and fail to clearly convey linguistic structure, and the cMculus as it stands is apparently not powerful enough to describe many phenomena en- countered in natural language. In this paper we suggest ways of dealing with both these deficiencies. Firstly, we reformulate Lambek's system using proof figures based on the 'natural de- duction' notation commonly used for derivations in logic, and discuss some of the related proof-theory. Natural deduction is generally regarded as the most economical and comprehensible system for working on proofs by hand, and we suggest that...