一种统一Lambek演算不同变体的超图逻辑导论

本文提出超图Lambek演算($\mathrm{HL}$)。该形式体系旨在将Lambek演算($\mathrm{L}$)推广到超图，正如超边替换文法扩展上下文无关文法那样。与Lambek演算不同，$\mathrm{HL}$处理超图类型与相继式；其公理与规则自然推广了$\mathrm{L}$的那些内容。因此，某些性质（例如割消去）可从$\mathrm{L}$提升到$\mathrm{HL}$。我们表明$\mathrm{L}$可自然嵌入$\mathrm{HL}$中；此外，其若干变体（$\mathrm{LP}$、$\mathrm{NL}$、$\mathrm{NLP}$、带模态的$\mathrm{L}$、$\mathrm{L}^\ast(\mathbf{1})$、$\mathrm{L}^{\mathrm{R}}$）也可通过不同的图构造嵌入$\mathrm{HL}$中。我们还建立了$\mathrm{HL}$与带内嵌蕴涵的Datalog之间的联系。我们证明了$\mathrm{HL}$的解析问题是NP完全的。