Abstract

We consider the task of theorem proving in Lambek calculi and their generalisation to ‘multimodal residuation calculi’. These form an integral part of categorial logic, a logic of signs stemming from categorial grammar, of the basis of which language processing is essentially theorem proving. The demand of this application is not just for efficient processing of some or other specific calculus, but for methods that will be generally applicable to categorial logics.It is proposed that multimodal cases be treated by dealing with the highest common factor of all the connectives as linear validity. The prosodic aspects are encoded in labels, in effect the term-structure of quantified linear logic. The correctness condition on proof nets can be implemented by SLD resolution in linear logic with unification on labels/terms limited to one way matching. A suitable unification strategy is obtained for calculi of discontinuity by normalisation of the ground goal term followed by recursive descent and redex pattern matching on the head term