粘合资源证明结构：居留问题与泰勒展开的逆操作
Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
AI总结：
本文提出新准则，通过重写系统刻画资源证明结构集合属于MELL证明结构泰勒展开的条件，并证明无切割MELL证明结构类型居留问题的半可判定性。
摘要：
乘法指数线性逻辑（MELL）证明结构可以展开为一组资源证明结构，即其泰勒展开。我们引入了一个新准则，通过一个同时作用于资源和MELL证明结构的重写系统，来刻画（并在有限情形下判定）那些属于某个MELL证明结构的泰勒展开的资源证明结构集合。我们还证明了无切割MELL证明结构的类型居留问题的半可判定性。
英文摘要：
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
