一句话：提出环归纳原则：若图是局部合流且（余）良基关系的对称闭包，则验证空环与局部合流环即可证明所有环的性质。
论文研究如何对图中的所有环（闭合链）证明性质。按环长度归纳不可行，因为环的真子链不一定是闭合的。作者考虑图是某个局部合流且（余）良基关系的对称闭包这一情形，提出一个类似归纳的证明原则。该原则表明：若待证性质足够“好”（在相关构造下保持），则只需证明空环满足性质，并证明由局部合流步骤生成的环满足性质，即可推出所有环都满足性质。这为需要处理闭合链与连贯性的证明提供了一般工具，避免对非闭合子链进行归纳。评估方式为数学证明：论文给出该证明原则的充分性论证，而非实验基准。
Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of induction for cycles for the case that the graph is given as the symmetric closure of a locally confluent and (co-)well-founded relation. We show that, assuming the property in question is sufficiently nice, it is enough to prove it for the empty cycle and for cycles given by local confluence.
DOI 原文 ·
@inproceedings{paperbot5519,
title = {Coherence via Well-Foundedness},
author = {Nicolai Kraus and Jakob von Raumer},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394800}
}