论文标题
循环证明，高音和及时闭合逻辑
Cyclic Proofs, Hypersequents, and Transitive Closure Logic
论文作者
论文摘要
我们根据一种高音形式提出了一个无剪裁的循环系统，用于及时闭合逻辑（TCL），适用于通过证明搜索自动推理。我们表明，先前提出的序列系统对于来自标准翻译的Kleene代数（KA）和命题动态逻辑（PDL）的基本有效性是不完整的。另一方面，我们的系统忠实地模拟了KA和PDL的已知循环系统，从而继承了它们的完整性结果。我们系统的特殊性是其更丰富的正确性标准，表现出“交替的痕迹”，并且需要比传统的循环证明更复杂的健全论点。
We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting 'alternating traces' and necessitating a more intricate soundness argument than for traditional cyclic proofs.
