Abstract
In this paper we study induction in the context of the firstorder μ-calculus with explicit approximations. We present and compare two Gentzen-style proof systems each using a different type of induction. The first is based on finite proof trees and uses a local well-founded induction rule, while the second is based on (finitely represented) ω-regular proof trees and uses a global induction discharge condition to ensure externally that all inductive reasoning is well-founded. We give effective procedures for the translation of proofs between the two systems, thus establishing their equivalence.
Research done mainly while at Swedish Institute of Computer Science (SICS), supported by Swiss European Fellowship 83EU-065536, and completed at INRIA, supported by an ERCIM fellowship.
Supported by the Swedish Research Council grant 621-2001-2637, “Semantics and Proof of Programming Languages”
As opposed to implicit induction (cf. [3]), based on Knuth-Bendix completion.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
T. Arts, G. Chuganov, M. Dam, L.-å. Fredlund, D. Gurov, and T. Noll. A tool for verifying software written in Erlang. Accepted for publication in STTT Journal, 2001.
G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 2000. to appear.
H. Comon. Inductionless induction. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, chapter 14. Elsevier Science, 2001.
M. Dam and D. Gurov. μ-calculus with explicit points and approximations. Journal of Logic and Computation, 12(2):43–57, 2002. Previously appeared in Fixed Points in Computer Science, FICS’ 02.
L. Fredlund. A Framework for Reasoning about Erlang Code. PhD thesis, Royal Institute of Technology, Stockholm, Sweden, 2001.
R. Goré. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods. Kluwer, 1999.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
D. Park. Finiteness is mu-ineffable. Theoretical Computer Science, 3(2):173–181, 1976.
C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. Technical Report 92-49, Laboratoire de l’Informatique du Parallélisme, ENS Lyon, France, Dec. 1992.
U. Schöpp. Formal verification of processes. Master’s thesis, University of Edinburgh, 2001.
U. Schöpp and A. Simpson. Verifying temporal properties using explicit approximants: Completeness for context-free processes. In FOSSACS’ 02, Grenoble, France, volume 2303 of LNCS, pages 372–386. Springer-Verlag, 2002.
A. Simpson and U. Schöpp. Private communication.
C. Stirling and D. Walker. Local model checking in the modal μ-calculus. Theoretical Computer Science, 89:161–177, 1991.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. Elsevier Science Publishers, Amsterdam, 1990.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Logic in Computer Science, LICS’ 86, pages 322–331, 1986.
I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. In Logic in Computer Science, LICS’ 95, pages 14–24, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sprenger, C., Dam, M. (2003). On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μCalculus. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_27
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive