Abstract
Logics based on the \(\mu \)-calculus are used to model inductive and coinductive reasoning and to verify reactive systems. A well-structured proof-theory is needed in order to apply such logics to the study of programming languages with (co)inductive data types and automated (co)inductive theorem proving. The traditional proof system suffers some defects, non-wellfounded (or infinitary) and circular proofs have been recognized as a valuable alternative, and significant progress have been made in this direction in recent years. Such proofs are non-wellfounded sequent derivations together with a global validity condition expressed in terms of progressing threads.
The present paper investigates a discrepancy found in such proof systems, between the sequential nature of sequent proofs and the parallel structure of threads: various proof attempts may have the exact threading structure while differing in the order of inference rules applications. The paper introduces infinets, that are proof-nets for non-wellfounded proofs in the setting of multiplicative linear logic with least and greatest fixed-points (\(\mu \mathsf {MLL}^{\infty }\)) and study their correctness and sequentialization.
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 754362. Partially funded by ANR Project RAPIDO, ANR-14-CE25-0007.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Baelde, D.: On the proof theory of regular fixed points. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 93–107. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02716-1_8
Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Computat. Logic (TOCL) 13(1), 2 (2012)
Baelde, D., Doumane, A., Kuperberg, D., Saurin, A.: Bouncing threads for infinitary and circular proofs. Manuscript, June 2019
Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille, France, 29 August–1 September 2016. LIPIcs, vol. 62, pp. 42:1–42:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)
Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 92–106. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75560-9_9
Bagnol, M., Doumane, A., Saurin, A.: On the dependencies of logical rules. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 436–450. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46678-0_28
Blute, R.F., Cockett, J.R.B., Seely, R.A.G., Trimble, T.H.: Natural deduction and coherence for weakly distributive categories. J. Pure Appl. Algebr. 113(3), 229–296 (1996)
Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh, November 2006
Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), Wroclaw, Poland, 10–12 July 2007, pp. 51–62. IEEE Computer Society (2007)
Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177–1216 (2011)
Clairambault, P.: Least and greatest fixpoints in game semantics. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 16–31. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00596-1_3
Curien, P.-L.: Introduction to linear logic and ludics, Part II (2006)
Danos, V.: Une application de la logique linéaire á l’étude des processus de normalisation (principalement du \(\lambda \)-calcul). Thèse de doctorat, Université Denis Diderot, Paris 7 (1990)
Danos, V., Regnier, L.: The structure of multiplicatives. Arch. Math. Log. 28, 181–203 (1989)
Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \(\mu \)-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273–284. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836_26
De, A., Saurin, A.: Infinets: the parallel syntax for non-wellfounded proof-theory. Long version, June 2019
Doumane, A.: On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes). Ph.D. thesis, Paris Diderot University, France (2017)
Doumane, A., Baelde, D., Hirschi, L., Saurin, A.: Towards completeness via proof search in the linear time \(\mu \)-calculus, January 2016. Accepted for publication at LICS
Fortier, J., Santocanale, L.: Cuts for circular proofs: semantics and cut-elimination. In: Della Rocca, S.R., (ed.) Computer Science Logic 2013 (CSL 2013), CSL, Torino, Italy, 2–5 September 2013. LIPIcs, vol. 23, pp. 248–262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)
Girard, J.-Y.: Proof-nets: the parallel syntax for proof theory (1996)
Guerrini, S.: A linear algorithm for mll proof net correctness and sequentialization. Theor. Comput. Sci. 412(20), 1958–1978 (2011)
Kaivola, R.: A simple decision method for the linear time mu-calculus. In: Desel, J. (ed.) Structures in Concurrency Theory. Workshops in Computing, pp. 190–204. Springer, London (1995). https://doi.org/10.1007/978-1-4471-3078-9_13
Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)
Melliès, P.-A.: Higher-order parity automata. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20–23 June 2017, pp. 1–12. IEEE Computer Society (2017)
Montelatici, R.: Polarized proof nets with cycles and fixpoints semantics. In: Hofmann, M. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 256–270. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44904-3_18
Park, D.: Fixpoint induction and proofs of program properties. Mach. Intell. 5, 59–78 (1969)
Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 357–371. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45931-6_25
Walukiewicz, I.: On completeness of the mu-calculus. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS 1993), Montreal, Canada, 19–23 June 1993, pp. 136–146. IEEE Computer Society (1993)
Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional mu-calculus. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, 26–29 June 1995, pp. 14–24. IEEE Computer Society (1995)
Acknowledgement
We are indebted to anonymous reviewers for providing insightful comments which has immensely enhanced the presentation of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
De, A., Saurin, A. (2019). Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory. In: Cerrito, S., Popescu, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2019. Lecture Notes in Computer Science(), vol 11714. Springer, Cham. https://doi.org/10.1007/978-3-030-29026-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-29026-9_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29025-2
Online ISBN: 978-3-030-29026-9
eBook Packages: Computer ScienceComputer Science (R0)