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.
Keywords: inductive reasoning, circular proofs, well-foundedness, global consistency condition, $\mu $-calculus, approximants
@article{ITA_2003__37_4_365_0,
author = {Sprenger, Christoph and Dam, Mads},
title = {On global induction mechanisms in a $\mu $-calculus with explicit approximations},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {365--391},
year = {2003},
publisher = {EDP-Sciences},
volume = {37},
number = {4},
doi = {10.1051/ita:2003024},
mrnumber = {2053032},
zbl = {1111.68518},
language = {en},
url = {http://geodesic.mathdoc.fr/articles/10.1051/ita:2003024/}
}
TY - JOUR AU - Sprenger, Christoph AU - Dam, Mads TI - On global induction mechanisms in a $\mu $-calculus with explicit approximations JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2003 SP - 365 EP - 391 VL - 37 IS - 4 PB - EDP-Sciences UR - http://geodesic.mathdoc.fr/articles/10.1051/ita:2003024/ DO - 10.1051/ita:2003024 LA - en ID - ITA_2003__37_4_365_0 ER -
%0 Journal Article %A Sprenger, Christoph %A Dam, Mads %T On global induction mechanisms in a $\mu $-calculus with explicit approximations %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2003 %P 365-391 %V 37 %N 4 %I EDP-Sciences %U http://geodesic.mathdoc.fr/articles/10.1051/ita:2003024/ %R 10.1051/ita:2003024 %G en %F ITA_2003__37_4_365_0
Sprenger, Christoph; Dam, Mads. On global induction mechanisms in a $\mu $-calculus with explicit approximations. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 365-391. doi: 10.1051/ita:2003024
Cité par Sources :