On global induction mechanisms in a µ-calculus with explicit approximations
On global induction mechanisms in a µ-calculus with explicit approximations
复制标题
具有显式近似的 µ 微积分中的全局归纳机制
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
M. Dam
中科院分区：
文献类型：
--
作者：
Christoph Sprenger;M. Dam
我们研究了基于循环证明的一阶 μ 微积分的 Gentzen 式证明系统，该系统通过展开定点公式并检测重复的证明目标而产生。我们的系统使用显式序数变量和近似来支持简单的语义归纳放电条件，从而确保归纳推理的有根据。作为本文的主要成果，我们提出了一种新的基于痕迹的句法放电条件，并建立了其与语义条件的等价性。我们给出了这个条件的自动机理论重新表述，它更适合实际证明。为了与以前的工作进行详细比较，我们考虑两个更简单的语法条件，并表明它们比我们的新条件更具限制性。
We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic condition. We give an automata-theoretic reformulation of this condition which is more suitable for practical proofs. For a detailed comparison with previous work we consider two simpler syntactic conditions and show that they are more restrictive than our new condition.