License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2018.35
URN: urn:nbn:de:0030-drops-97025
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9702/
Nollet, Rémi ;
Saurin, Alexis ;
Tasson, Christine
Local Validity for Circular Proofs in Linear Logic with Fixed Points
Abstract
Circular (ie. non-wellfounded but regular) proofs have received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of non-wellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. pre-proofs), those which are logically valid proofs. A standard approach is to consider a pre-proof 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 Brotherston-Simpson 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:1--35:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Dan Ghica and Achim Jung},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9702},
URN = {urn:nbn:de:0030-drops-97025},
doi = {10.4230/LIPIcs.CSL.2018.35},
annote = {Keywords: sequent calculus, non-wellfounded proofs, circular proofs, induction, coinduction, fixed points, proof-search, linear logic, muMALL, finitization, inf}
}
|
Keywords: |
|
sequent calculus, non-wellfounded proofs, circular proofs, induction, coinduction, fixed points, proof-search, linear logic, muMALL, finitization, inf |
|
Collection: |
|
27th EACSL Annual Conference on Computer Science Logic (CSL 2018) |
|
Issue Date: |
|
2018 |
|
Date of publication: |
|
29.08.2018 |
