×

On the structure of inductive reasoning: Circular and tree-shaped proofs in the \(\mu\)-calculus. (English) Zbl 1029.03016

Gordon, Andrew D. (ed.), Foundations of software science and computations structure. 6th international conference, FOSSACS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2620, 425-440 (2003).
Summary: In this paper we study induction in the context of the first-order \(\mu\)-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) \(\omega\)-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.
For the entire collection see [Zbl 1017.00036].

MSC:

03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
03F07 Structure of proofs
PDFBibTeX XMLCite
Full Text: Link