1. Infinets: The parallel syntax for non-wellfounded proof-theory
- Author
-
Abhishek De, Alexis Saurin, Université Paris Diderot - Paris 7 (UPD7), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), This project has received funding from the European Union’s Horizon 2020 researchand innovation programme under the Marie Sklodowska-Curie grant agreement No754362. Partially funded by ANR Project RAPIDO, ANR-14-CE25-0007., ANR-14-CE25-0007,RAPIDO,Raisonner et Programmer avec des Données Infinies(2014), De, Abhishek, Preuves, Programmes et Systèmes (PPS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7), and Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)
- Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ,Computer science ,Proof-net ,Linear logic ,0102 computer and information sciences ,02 engineering and technology ,Mathematical proof ,01 natural sciences ,Data type ,Computer Science::Logic in Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,Calculus ,Mu-calculus ,Sequent ,Induction and coinduction ,Syntax (programming languages) ,Coinduction ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Circular proofs ,Fixed points ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Proof theory ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Non-wellfounded proofs ,020201 artificial intelligence & image processing ,Proof net - Abstract
Logics based on the µ-calculus are used to model induc-tive 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. While 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 (µMLL ∞) and study their correctness and sequentialization. Inductive and coinductive reasoning is pervasive in computer science to specify and reason about infinite data as well as reactive properties. Developing appropriate proof systems amenable to automated reasoning over (co)inductive statements is therefore important for designing programs as well as for analyzing computational systems. Various logical settings have been introduced to reason about such inductive and coinductive statements, both at the level of the logical languages modelling (co)induction (such as Martin Löf's inductive predicates or fixed-point logics, also known as µ-calculi) and at the level of the proof-theoretical framework considered (finite proofs with explicit (co)induction rulesà la Park [23] or infinite, non-wellfounded proofs with fixed-point unfold-ings) [6-8, 4, 1, 2]. Moreover, such proof systems have been considered over classical logic [6, 8], intuitionistic logic [9], linear-time or branching-time temporal logic [19, 18, 25, 26, 13-15] or linear logic [24, 16, 4, 3, 14].
- Published
- 2019