Extractability as the Deduction Theorem in Subdirectional Combinatory Logic

作者: Hiroko Ozaki , Daisuke Bekki

DOI: 10.1007/978-3-642-31262-5_13

关键词:

摘要: The formulation of Combinatory Categorial Grammar (CCG) [7], especially the choice combinatory rules and their nominatum, strongly imply connection with a typed-version Logic (CL). Since typed CL is term calculus for an implication fragment Hilbert-style proof system, in sense Curry-Howard isomorphism, it seems plausible to regard CCG as grammar that corresponds associative Lambek [3] Gentzen-style system.

参考文章(7)
Daisuke Bekki, Combinatory categorial grammar as a substructural logic: preliminary remarks international symposium on artificial intelligence. pp. 16- 29 ,(2010) , 10.1007/978-3-642-25655-4_3
Mark Steedman, The syntactic process ,(2000)
Jonathan P. Seldin, J. Roger Hindley, Lambda-Calculus and Combinators: An Introduction ,(2008)
Joachim Lambek, The Mathematics of Sentence Structure American Mathematical Monthly. ,vol. 65, pp. 154- 170 ,(1958) , 10.1080/00029890.1958.11989160
Glyn V. Morrill, Type Logical Grammar Springer Netherlands. ,(1994) , 10.1007/978-94-011-1042-6
J. Roger Hindley, Jonathan P. Seldin, Lambda-Calculus and Combinators, an Introduction Cambridge University Press. ,(2008) , 10.1017/CBO9780511809835
The Mathematics of Sentence Structure The American Mathematical Monthly. ,vol. 65, pp. 154- None ,(1958) , 10.2307/2310058