Logical foundations for hybrid type-logical grammars
This is an incremental theoretical contribution for computational linguists and logicians working on formal grammar systems.
This paper establishes the logical foundations for hybrid type-logical grammars by proving properties like normalization and the subformula property, and presents both sequent and proof net calculi for the system. The work clarifies the theoretical underpinnings and enables future extensions such as non-associative and multimodal versions.
This paper explores proof-theoretic aspects of hybrid type-logical grammars , a logic combining Lambek grammars with lambda grammars. We prove some basic properties of the calculus, such as normalisation and the subformula property and also present both a sequent and a proof net calculus for hybrid type-logical grammars. In addition to clarifying the logical foundations of hybrid type-logical grammars, the current study opens the way to variants and extensions of the original system, including but not limited to a non-associative version and a multimodal version incorporating structural rules and unary modes.