Tableau Algorithms for Categorial Deduction and Parsing

Abstract

In this thesis we develop automated dedution mehanisms designed to keep complexity of categorial parsing under control while preserving the levels of uniformity and coverage one finds in labeled dedutive systems. First,we define the hierarhy of caluli whose computational treatment is addresed in the thesis,review the main issues and linguistic motivations behind proof-theoretical features of each calculus and describe the correspondence between proofs and semantic interpretation with respect to lambda terms.

Next we introduce the rules and algorithms of a deductive system based on analytic tableaux which covers the whole hierarchy of categorial calculi presented.Completenes and termination results are shown. We then impose syntactic constraints on the calculi and elaborate label unification proceedures aimed at limiting the system's complexity. Alternative proof-search strategies are discussed and a technique for recovering syntactic structure from tableau derivations is developed. In the last chapters we compare our system with other methods used in categorial deduction,discuss design issues,heuristics and extensions,and link categorial deduction with theorem proving in recently developed logics of information flow such as channel theory.