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
Number of Authors: 2
2003 (English)Conference 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.
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-22439ISBN: 3-540-00897-7 (print)OAI: oai:DiVA.org:ri-22439DiVA: diva2:1041984
Conference
Proceedings of 6th International Conference, Foundations of Software Science and Computational Structures (FOSSACS)
Note
http://www.sics.se/~mfd/fossacs03.ps. Lecture Notes in Computer Science; 2620. Springer 2003, ISBN 3-540-00897-7.Available from: 2016-10-31 Created: 2016-10-31Bibliographically approved

Open Access in DiVA

No full text

Other links

http
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

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.26.0