论文标题
NL $λ$的证明理论方面
Proof-theoretic aspects of NL$λ$
论文作者
论文摘要
我们提供了逻辑NL $λ$的证明理论分析（Barker \＆Shan 2014，Barker 2019）。我们值得注意的是，我们引入了一种新颖的证明网微积分，并证明与逻辑的序列演算相对于逻辑的序列有声音和完整。我们使用这种新的演算研究了逻辑的可决定性和复杂性，证明了逻辑复杂性的新上限（表明它在NP中），以及形式主义产生的正式语言类别的新下限（在上下文敏感的语言中使用置换封闭的操作扩展）。最后，由于这个新的演算，我们提出了NL $λ$与Kubota \＆Levine（2020）的混合型型语法之间的新颖比较。我们表明，在两种形式主义中提出的自然语言分析存在意想不到的融合。除了研究NL $λ$的证明理论特性外，我们还大大扩展了其语言覆盖范围。
We present a proof-theoretic analysis of the logic NL$λ$ (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$λ$ 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$λ$, we greatly extends its linguistic coverage.
