Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On the structure of inductive reasoning: circular and tree-shaped proofs in the mu-calculus
RISE, Swedish ICT, SICS.
2003 (English)In: Proceedings of 6th International Conference, Foundations of Software Science and Computational Structures (FOSSACS), 2003, 1, , 16 p.Conference paper, Published paper (Refereed)
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, 1. , 16 p.
Series
LNCS, 2620
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:ri:diva-22439ISBN: 3-540-00897-7 (print)OAI: oai:DiVA.org:ri-22439DiVA: diva2:1041984
Conference
6th International Conference, Foundations of Software Science and Computational Structures (FOSSACS), 7-11 April 2003, Warsaw, Poland
Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-01-14Bibliographically approved

Open Access in DiVA

No full text

Other links

http://www.springerlink.com/content/150j5vejxy3h6t3a/
By organisation
SICS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
v. 2.30.0