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.

翻译：一个多倍、多倍、多值线性逻辑(MELL)验证结构可以扩大为一套资源验证结构:其泰勒的扩张。我们引入了一种新的标准,将作为泰勒扩大某些多值线性线性逻辑(MELL)验证结构的一部分的一组资源验证结构定性为(并在有限的情况下决定),通过对资源和多值线性线性逻辑验证结构同时起作用的重写系统进行扩展。我们还证明,对于零切的 MELL验证结构而言,类型居住问题具有半衰减性。