具有次指数和次幂模态的乘加型Lambek演算
The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities
摘要：
我们给出了一个证明理论和算法的复杂性分析系统介绍Morrill作为核心的CatLog类别语法分析器。我们考虑两个最近版本的莫里尔的演算，并专注于他们的片段，包括乘法（兰贝克）连接词，加法连接和析取，括号和括号模态，和!次指数模态对于这两个系统，我们解决的问题与切割规则，并提供必要的修改，之后，我们证明了可接受的削减（削减消除定理）。我们还证明了演算的不可判定性，并表明基于它们的范畴语法可以生成任意递归可判定语言。
英文摘要：
We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill's calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the ! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
