Geodesic
On global induction mechanisms in a μ-calculus with explicit approximations
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 365-391

Voir la notice de l'article provenant de la source Numdam

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.

DOI : 10.1051/ita:2003024
Classification : 68Q60, 03F07, 03B35
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},
     publisher = {EDP-Sciences},
     volume = {37},
     number = {4},
     year = {2003},
     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 :