Nollet, Rémi ;
Saurin, Alexis ;
Tasson, Christine
Local Validity for Circular Proofs in Linear Logic with Fixed Points
Abstract
Circular (ie. nonwellfounded but regular) proofs have received increasing interest in recent years with the simultaneous development of their applications and metatheory: infinitary proof theory is now wellestablished in several prooftheoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of nonwellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. preproofs), those which are logically valid proofs. A standard approach is to consider a preproof to be valid if every infinite branch is supported by an infinitely progressing thread.
The paper focuses on circular proofs for MALL with fixed points. Among all representations of valid circular proofs, a new fragment is described, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's muMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently. Moreover the BrotherstonSimpson conjecture holds for this fragment: every labelled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs.
BibTeX  Entry
@InProceedings{nollet_et_al:LIPIcs:2018:9702,
author = {R{\'e}mi Nollet and Alexis Saurin and Christine Tasson},
title = {{Local Validity for Circular Proofs in Linear Logic with Fixed Points}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {35:135:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770880},
ISSN = {18688969},
year = {2018},
volume = {119},
editor = {Dan Ghica and Achim Jung},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9702},
URN = {urn:nbn:de:0030drops97025},
doi = {10.4230/LIPIcs.CSL.2018.35},
annote = {Keywords: sequent calculus, nonwellfounded proofs, circular proofs, induction, coinduction, fixed points, proofsearch, linear logic, muMALL, finitization, inf}
}
29.08.2018
Keywords: 

sequent calculus, nonwellfounded proofs, circular proofs, induction, coinduction, fixed points, proofsearch, linear logic, muMALL, finitization, inf 
Seminar: 

27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Issue date: 

2018 
Date of publication: 

29.08.2018 