Grammar specification in categorial logics and theorem proving

Abstract

This paper presents an application of automated theorem proving techniques to natural language processing, particularly to Categorial Grammar (CG) parsing. It describes the system LLKE, a labelled analytic tableau system which supports a framework for specification and proof for several calculi, starting with the Lambek calculus L, covering its substructural extensions such as LP, LPE, LPE, NL etc, and allowing for the implementation of modalities. The tableau expansion algorithms are presented and heuristics to improve their performance based on domain-specific knowledge are discussed along with comparisons of our system with other systems that implement categorial deduction.