文档介绍：Categorial Type Logics
Michael Moortgat
Utrecht Institute of Linguistics, OTS
Excerpt from Chapter Two in J. van Benthem and A. ter Meulen (eds.)
Handbook of Logic and Language. Elsevier, 1997.
Contents
1 Introduction: grammatical reasoning 1
2 Linguistic inference: the Lambek systems 5
............................ 5
Gentzen calculus, cut elimination and decidability . . . . . . . . . . . . . . . . . . . . 9
Discussion: options for resource management . . . . . . . . . . . . . . . . . . . . . . 13
3 The syntax-semantics interface: proofs and readings 16
Term assignment for categorial deductions . . . . . . . . . . . . . . . . . . . . . . . . 17
Natural language interpretation: the deductive view . . . . . . . . . . . . . . . . . . . 21
4 position: multimodal systems 26
:position........................ 26
:unaryoperations....................... 30
Unary connectives: logic and structure . . . . . . . . . . . . . . . . . . . . . . . 31
Applications: imposing constraints, structural relaxation . . . . . . . . . . . . 35
Resource control: faithful embeddings . . . . . . . . . . . . . . . . . . . . . . . 38
5 Reasoning about multiple type assignments 40
6Hybridarchitectures 40
7 Categorial parsing as deduction 41
8 Conclusions, directions for further research 41
i
Definitions
(5) Binary multiplicatives: formula language.
() Binary multiplicatives: frame semantics.
() The pure residuation logic NL.
() Canonical model.
() Resource management postulates.
() Weak Sahlqvist axioms.
(6) Groupoid interpretation.
() Combinator proof terms.
() Gentzen calculus: NL.
(8) Gentzen calculus: structural rules.
() Implicit structural rules.
(9) The Cut rule.
() Natural Deduction.
(11) Lifting as closure operation.
(13) Semantic domains.
() Syntax of typed λ terms.
() Term assignment: LP.
() LP proof terms.