2 Search Results for "Leitsch, Alexander"

Document
DOI: 10.4230/LIPIcs.CSL.2025.32
A Mixed Linear and Graded Logic: Proofs, Terms, and Models

Authors: Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality !_r captures how many times a proposition is used and has an analogous interpretation to the of-course modality from linear logic; the of-course modality from linear logic can be modelled by a linear exponential comonad and graded of-course can be modelled by a graded linear exponential comonad. Benton showed in his seminal paper on Linear/Non-Linear logic that the of-course modality can be split into two modalities connecting intuitionistic logic with linear logic, forming a symmetric monoidal adjunction. Later, Fujii et al. demonstrated that every graded comonad can be decomposed into an adjunction and a "strict action". We give a similar result to Benton, leveraging Fujii et al.’s decomposition, showing that graded modalities can be split into two modalities connecting a graded logic with a graded linear logic. We propose a sequent calculus, its proof theory and categorical model, and a natural deduction system which we show is isomorphic to the sequent calculus system. Interestingly, our system can also be understood as Linear/Non-Linear logic composed with an action that adds the grading, further illuminating the shared principles between linear logic and a class of graded modal logics.
Cite as

Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard. A Mixed Linear and Graded Logic: Proofs, Terms, and Models. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vollmer_et_al:LIPIcs.CSL.2025.32,
  author =	{Vollmer, Victoria and Marshall, Danielle and Eades III, Harley and Orchard, Dominic},
  title =	{{A Mixed Linear and Graded Logic: Proofs, Terms, and Models}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{32:1--32:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.32},
  URN =		{urn:nbn:de:0030-drops-227892},
  doi =		{10.4230/LIPIcs.CSL.2025.32},
  annote =	{Keywords: linear logic, graded modal logic, adjoint decomposition}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.485
Towards CERes in intuitionistic logic

Authors: Alexander Leitsch, Giselle Reis, and Bruno Woltzenlogel Paleo

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Cut-elimination, introduced by Gentzen, plays an important role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas), resulting in an analytic proof. CERes is a method of cut-elimination by resolution that relies on global proof transformations, in contrast to reductive methods, which use local proof-rewriting transformations. By avoiding redundant operations, it obtains a speed-up over Gentzen's traditional method (and its variations). CERes has been successfully implemented and applied to mathematical proofs, and it is fully developed for classical logic (first and higher order), multi-valued logics and Gödel logic. But when it comes to mathematical proofs, intuitionistic logic also plays an important role due to its constructive characteristics and computational interpretation. This paper presents current developments on adapting the CERes method to intuitionistic sequent calculus LJ. First of all, we briefly describe the CERes method for classical logic and the problems that arise when extending the method to intuitionistic logic. Then, we present the solutions found for the mentioned problems for the subclass LJ- (the class of intuitionistic proofs of an end-sequent containing no strong quantifiers and no formula on the right). In addition, we explain, with an example, some ideas for improving the method and covering a bigger fragment of LJ proofs. Finally, we summarize the results and point the direction for future research.
Cite as

Alexander Leitsch, Giselle Reis, and Bruno Woltzenlogel Paleo. Towards CERes in intuitionistic logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 485-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{leitsch_et_al:LIPIcs.CSL.2012.485,
  author =	{Leitsch, Alexander and Reis, Giselle and Woltzenlogel Paleo, Bruno},
  title =	{{Towards CERes in intuitionistic logic}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{485--499},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.485},
  URN =		{urn:nbn:de:0030-drops-36922},
  doi =		{10.4230/LIPIcs.CSL.2012.485},
  annote =	{Keywords: cut-elimination, resolution, LJ}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2012

  • Refine by Author
  • 1 Eades III, Harley
  • 1 Leitsch, Alexander
  • 1 Marshall, Danielle
  • 1 Orchard, Dominic
  • 1 Reis, Giselle
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Logic

  • Refine by Keyword
  • 1 LJ
  • 1 adjoint decomposition
  • 1 cut-elimination
  • 1 graded modal logic
  • 1 linear logic
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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