Extractability as the Deduction Theorem in Subdirectional Combinatory Logic
Autor: | Daisuke Bekki, Hiroko Ozaki |
---|---|
Rok vydání: | 2012 |
Předmět: |
Discrete mathematics
Deduction theorem Categorial grammar Fragment (logic) Computer Science::Logic in Computer Science Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing) Combinatory categorial grammar Term (logic) Combinatory logic Algorithm Curry–Howard correspondence Associative property Mathematics |
Zdroj: | Logical Aspects of Computational Linguistics ISBN: 9783642312618 LACL |
DOI: | 10.1007/978-3-642-31262-5_13 |
Popis: | The formulation of Combinatory Categorial Grammar (CCG) [7], especially the choice of combinatory rules and their nominatum, strongly imply connection with a typed-version of Combinatory Logic (CL). Since typed CL is a term calculus for an implication fragment of a Hilbert-style proof system, in the sense of the Curry-Howard isomorphism, it seems plausible to regard CCG as a grammar that corresponds to a Hilbert-style proof system, in that the associative Lambek calculus [3] corresponds to a Gentzen-style proof system. |
Databáze: | OpenAIRE |
Externí odkaz: |