一句话：用重写系统刻画资源证明结构集何时来自 MELL 证明结构的 Taylor 展开，并证明无割 MELL 居留问题半可判定。
本文研究乘法-指数线性逻辑（MELL）证明结构与 Taylor 展开的关系。一个 MELL 证明结构可展开为一组资源证明结构，即其 Taylor 展开。作者引入一种新准则，借助同时作用于资源证明结构与 MELL 证明结构的重写系统，刻画哪些资源证明结构集合是某个 MELL 证明结构的 Taylor 展开的一部分；在有限情形下，该准则可判定。论文还证明无割 MELL 证明结构的类型居留（inhabitation）问题是半可判定的。关键结果给出了 Taylor 展开的逆向刻画，并把资源重写与 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.
@article{paperbot1707,
title = {Gluing resource proof-structures: inhabitation and inverting the Taylor expansion},
author = {Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:4)2022}
}