scientific article; zbMATH DE number 1421203
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].
- Language and proof theory. Preface to the special issue on ``Proof theory and natural language
- Should pregroup grammars be adorned with additional operations?
- Deductive and grammatical competence: type logical remarks on nesting phenomena
- On Commutative and Nonassociative Syntactic Calculi and Categorial Grammars
- Talking about Explicit Databases in Categorial Grammar
- Some 3-Dimensional Systems of Labelled Deduction
- Labelled proof nets for the syntax and semantics of natural languages
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4946232)
