Proof-theoretic aspects of NL$λ$
We present a proof-theoretic analysis of the logic NL$\lambda$ (Barker \& Shan 2014, Barker 2019). We notably introduce a novel calculus of proof nets and prove it is sound and complete with respect to the sequent calculus for the logic. We study decidability and complexity of the logic using this new calculus, proving a new upper bound for complexity of the logic (showing it is in NP) and a new lower bound for the class of formal language generated by the formalism (mildly context-sensitive languages extended with a permutation closure operation). Finally, thanks to this new calculus, we present a novel comparison between NL$\lambda$ and the hybrid type-logical grammars of Kubota \& Levine (2020). We show there is an unexpected convergence of the natural language analyses proposed in the two formalism. In addition to studying the proof-theoretic properties of NL$\lambda$, we greatly extends its linguistic coverage.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Partial Orders, Residuation, and First-Order Linear Logic
We will investigate proof-theoretic and linguistic aspects of first-order linear logic. We will show that adding partial order constraints in such a way that each sequent defines a unique linear order on the antecedent f…
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving
This volume of EPTCS contains the proceedings of the Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), held on September 23-24, 2017 as part of the Tableaux, FroCoS and ITP conferences in Brasilia, Brazil…
Automated Theorem ProvingLogical foundations for hybrid type-logical grammars
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 subformu…
Vocal Bursts Type PredictionWhat Makes for Good Image Captions?
This paper establishes a formal information-theoretic framework for image captioning, conceptualizing captions as compressed linguistic representations that selectively encode semantic units in images. Our framework posi…
HallucinationImage CaptioningRepresentation LearningMeasurability in the Fundamental Theorem of Statistical Learning
The Fundamental Theorem of Statistical Learning states that a hypothesis space is PAC learnable if and only if its VC dimension is finite. For the agnostic model of PAC learning, the literature so far presents proofs of …
Binary ClassificationPAC learning