No label defined (Q4946232)

The paper is devoted to the presentation of a uniform algorithmic proof theory for the structure-sensitive style of grammatical reasoning in terms of Gabbay's framework of Labelled Deduction. The research connected with composition of form and meaning in natural language was initiated by J. Lambek. In Section 1 a brief overview of the grammatical architecture assumed in the paper is presented. In the next section the author presents two systems of labelled deduction for the display of derivations in the extended categorial logics. The first one is a categorical presentation of the system described by J. Lambek in the paper ``Categorial and categorical grammar'' (1988). The second one is natural deduction with the Curry-Howard labelling. In this section one can also find a linguistic illustration on the basis of labelled natural deduction formats. Such formats are useful for displaying known proofs, but their disadvantage is the fact that they do not have the right properties for algorithmic proof search. Section 3 provides the above-mentioned uniform algorithmic proof theory. Systems of labelled Gentzen calculus and labelled proof nets are presented. For the entire collection see [Zbl 0927.00010].