新论文 · v1arXiv:2611.04788
Global Trace Condition for Injective Transition Graphs
Stefano Berardi, Ugo de'Liguoro, Daniel Osorio-Valencia
We formulate the global trace condition, GTC, for cyclic proofs as a particular case of the size-change termination condition, or SCT. We express cyclic proofs through a variant of size-change graphs, called transition graphs, whose edges are labelled by (finite) bipartite relations. We show that injective transition graphs suffice to encode cyclic pre-proofs for a variant of Brotherston and Simpson's sequent calculus with inductive definitions. The injectivity of transition graphs corresponds to restricting SCT to fan-in-free graphs. Then we prove that an essentially weaker condition implies SCT in this case, and hence GTC.
尚无 AI 解读，展示原文摘要
cs.LO