5 Search Results for "Avron, Arnon"

Document
DOI: 10.4230/LIPIcs.CSL.2026.19
A Unifying Conservation Theorem

Authors: Giulio Fellin

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The relationship between classical and constructive logics has long been illuminated by a series of conservation results, beginning with Kolmogorov’s negative translation and Glivenko’s double negation theorem, and later extended by Kuroda and Segerberg to first-order and minimal logics respectively. These results reveal how certain classical principles can be interpreted or recovered within weaker constructive frameworks, either via translations or through minimal extensions that satisfy specific logical properties. In this paper, we propose a unifying generalisation of these conservation theorems, that consolidates and expands the abstract methods introduced in earlier studies, offering a unified perspective on the interplay between classical provability and constructive reasoning.
Cite as

Giulio Fellin. A Unifying Conservation Theorem. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fellin:LIPIcs.CSL.2026.19,
  author =	{Fellin, Giulio},
  title =	{{A Unifying Conservation Theorem}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.19},
  URN =		{urn:nbn:de:0030-drops-254431},
  doi =		{10.4230/LIPIcs.CSL.2026.19},
  annote =	{Keywords: double negation, negative translation, conservation, minimal logic, Glivenko’s theorem}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.34
Monad Translations for Higher-Order Logic

Authors: Thomas Traversié

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Classical logic can be embedded into intuitionistic logic by inserting double negations in formulas. Several translations generalize this idea by using monad operators instead of double negations. They eliminate particular axioms, for instance the principle of excluded middle or the principle of explosion, and therefore can be used to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic. Such translations have been defined for first-order logic. In this paper, we define a translation, parameterized by monad operators, for higher-order logic. In particular, the property that any formula and its translation are equivalent in the presence of the eliminated axiom holds under functional extensionality and propositional extensionality. We apply this translation to embed higher-order classical (respectively intuitionistic) logic into higher-order intuitionistic (respectively minimal) logic. By adapting Friedman’s trick, we show that coherent formulas correspond to a constructive fragment of higher-order classical logic, meaning that we can transform classical proofs into intuitionistic proofs without modifying the proven statements.
Cite as

Thomas Traversié. Monad Translations for Higher-Order Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{traversie:LIPIcs.FSCD.2025.34,
  author =	{Traversi\'{e}, Thomas},
  title =	{{Monad Translations for Higher-Order Logic}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{34:1--34:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.34},
  URN =		{urn:nbn:de:0030-drops-236495},
  doi =		{10.4230/LIPIcs.FSCD.2025.34},
  annote =	{Keywords: Higher-order logic, Intuitionistic logic, Kuroda’s translation, Monad}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.42
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Authors: Tim S. Lyon

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

Abstract
We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini’s sequent system GL_{seq}, Shamkanov’s non-wellfounded and cyclic sequent systems GL_∞ and GL_{circ}, Poggiolesi’s tree-hypersequent system CSGL, and Negri’s labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GL_{seq}, GL_∞, and GL_{circ}, and Goré and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GL_{seq} and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GL_{seq}, GL_∞, GL_{circ}, CSGL, G3GL, and LNGL while also giving (to the best of the author’s knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.
Cite as

Tim S. Lyon. Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lyon:LIPIcs.CSL.2025.42,
  author =	{Lyon, Tim S.},
  title =	{{Unifying Sequent Systems for G\"{o}del-L\"{o}b Provability Logic via Syntactic Transformations}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{42:1--42:23},
  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.42},
  URN =		{urn:nbn:de:0030-drops-227992},
  doi =		{10.4230/LIPIcs.CSL.2025.42},
  annote =	{Keywords: Cyclic proof, G\"{o}del-L\"{o}b logic, Labeled sequent, Linear nested sequent, Modal logic, Non-wellfounded proof, Proof theory, Proof transformation, Tree-hypersequent}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.8
Safety, Absoluteness, and Computability

Authors: Arnon Avron, Shahar Lev, and Nissan Levi

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The semantic notion of dependent safety is a common generalization of the notion of absoluteness used in set theory and the notion of domain independence used in database theory for characterizing safe queries. This notion has been used in previous works to provide a unified theory of constructions and operations as they are used in different branches of mathematics and computer science, including set theory, computability theory, and database theory. In this paper we provide a complete syntactic characterization of general first-order dependent safety. We also show that this syntactic safety relation can be used for characterizing the set of strictly decidable relations on the natural numbers, as well as for characterizing rudimentary set theory and absoluteness of formulas within it.
Cite as

Arnon Avron, Shahar Lev, and Nissan Levi. Safety, Absoluteness, and Computability. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{avron_et_al:LIPIcs.CSL.2018.8,
  author =	{Avron, Arnon and Lev, Shahar and Levi, Nissan},
  title =	{{Safety, Absoluteness, and Computability}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.8},
  URN =		{urn:nbn:de:0030-drops-96754},
  doi =		{10.4230/LIPIcs.CSL.2018.8},
  annote =	{Keywords: Dependent Safety, Computability, Absoluteness, Decidability, Domain Independence}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.7
Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency

Authors: Ofer Arieli and Arnon Avron

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Paradefinite (`beyond the definite') logics are logics that can be used for handling contradictory or partial information. As such, paradefinite logics should be both paraconsistent and paracomplete. In this paper we consider the simplest semantic framework for defining paradefinite logics, consisting of four-valued matrices, and study the better accepted logics that are induced by these matrices.
Cite as

Ofer Arieli and Arnon Avron. Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{arieli_et_al:LIPIcs.FSCD.2016.7,
  author =	{Arieli, Ofer and Avron, Arnon},
  title =	{{Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.7},
  URN =		{urn:nbn:de:0030-drops-59731},
  doi =		{10.4230/LIPIcs.FSCD.2016.7},
  annote =	{Keywords: Paraconsistecy, Paracompleteness, 4-valued logics}
}
  • Refine by Type
  • 5 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 1 2018
  • 1 2016

  • Refine by Author
  • 2 Avron, Arnon
  • 1 Arieli, Ofer
  • 1 Fellin, Giulio
  • 1 Lev, Shahar
  • 1 Levi, Nissan
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Proof theory
  • 2 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Models of computation

  • Refine by Keyword
  • 1 4-valued logics
  • 1 Absoluteness
  • 1 Computability
  • 1 Cyclic proof
  • 1 Decidability
  • 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