Change search
ReferencesLink to record
Permanent link

Direct link
On global induction mechanisms in a mu-calculus with explicit approximations
KTH, Superseded Departments, Microelectronics and Information Technology, IMIT.ORCID iD: 0000-0001-5432-6442
2003 (English)In: Informatique théorique et applications (En ligne), ISSN 1290-385X, Vol. 37, no 4, 365-391 p.Article in journal (Refereed) Published
Abstract [en]

We investigate a Gentzen-style proof system for the first-order mu-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.

Place, publisher, year, edition, pages
2003. Vol. 37, no 4, 365-391 p.
Keyword [en]
inductive reasoning, circular proofs, well-foundedness, global consistency condition, mu-calculus, approximants, local model checking
URN: urn:nbn:se:kth:diva-23303ISI: 000220666900006OAI: diva2:342001
QC 20100525Available from: 2010-08-10 Created: 2010-08-10Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Dam, Mads
By organisation
Microelectronics and Information Technology, IMIT
In the same journal
Informatique théorique et applications (En ligne)

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 12 hits
ReferencesLink to record
Permanent link

Direct link