4 Search Results for "Acclavio, Matteo"

Document
DOI: 10.4230/LIPIcs.CSL.2024.8
Infinitary Cut-Elimination via Finite Approximations

Authors: Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.
Cite as

Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary Cut-Elimination via Finite Approximations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.CSL.2024.8,
  author =	{Acclavio, Matteo and Curzi, Gianluca and Guerrieri, Giulio},
  title =	{{Infinitary Cut-Elimination via Finite Approximations}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.8},
  URN =		{urn:nbn:de:0030-drops-196510},
  doi =		{10.4230/LIPIcs.CSL.2024.8},
  annote =	{Keywords: cut-elimination, non-wellfounded proofs, parsimonious logic, linear logic, proof theory, approximation, sequent calculus, non-uniform proofs}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.22
A Graphical Proof Theory of Logical Time

Authors: Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV.
Cite as

Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger. A Graphical Proof Theory of Logical Time. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 22:1-22:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.FSCD.2022.22,
  author =	{Acclavio, Matteo and Horne, Ross and Mauw, Sjouke and Stra{\ss}burger, Lutz},
  title =	{{A Graphical Proof Theory of Logical Time}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{22:1--22:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.22},
  URN =		{urn:nbn:de:0030-drops-163037},
  doi =		{10.4230/LIPIcs.FSCD.2022.22},
  annote =	{Keywords: proof theory, causality, deep inference}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.14
New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial

Authors: Anupam Das and Alex A. Rice

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems. Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : x ∧ (y ∨ z) → (x ∧ y) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger.
Cite as

Anupam Das and Alex A. Rice. New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.FSCD.2021.14,
  author =	{Das, Anupam and Rice, Alex A.},
  title =	{{New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.14},
  URN =		{urn:nbn:de:0030-drops-142525},
  doi =		{10.4230/LIPIcs.FSCD.2021.14},
  annote =	{Keywords: rewriting, linear inference, proof theory, linear logic, implementation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.6
Generalized Connectives for Multiplicative Linear Logic

Authors: Matteo Acclavio and Roberto Maieli

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions. We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.
Cite as

Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.CSL.2020.6,
  author =	{Acclavio, Matteo and Maieli, Roberto},
  title =	{{Generalized Connectives for Multiplicative Linear Logic}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.6},
  URN =		{urn:nbn:de:0030-drops-116490},
  doi =		{10.4230/LIPIcs.CSL.2020.6},
  annote =	{Keywords: Linear Logic, Partitions Sets, Proof Nets, Sequent Calculus}
}
  • Refine by Author
  • 3 Acclavio, Matteo
  • 1 Curzi, Gianluca
  • 1 Das, Anupam
  • 1 Guerrieri, Giulio
  • 1 Horne, Ross
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Linear logic
  • 3 Theory of computation → Proof theory
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Process calculi

  • Refine by Keyword
  • 3 proof theory
  • 2 linear logic
  • 1 Linear Logic
  • 1 Partitions Sets
  • 1 Proof Nets
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2020
  • 1 2021
  • 1 2022
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact