5 Search Results for "Santocanale, Luigi"

Document
DOI: 10.4230/LIPIcs.ISAAC.2025.24
Enumerating the Irreducible Closed Sets of an Acyclic Implicational Base of Bounded Degree

Authors: Oscar Defrain, Arthur Ohana, and Simon Vilmin

Published in: LIPIcs, Volume 359, 36th International Symposium on Algorithms and Computation (ISAAC 2025)

Abstract
We consider the problem of enumerating the irreducible closed sets of a closure system given by an implicational base. To date, the complexity status of this problem is widely open, and it is further known to generalize the notorious hypergraph dualization problem, even in the case of acyclic convex geometries, i.e., closure systems admitting an acyclic implicational base. This paper studies this case with a focus on the degree, which corresponds to the maximal number of implications in which an element occurs. We show that the problem is tractable for bounded values of this parameter, even when relaxed to the notions of premise- and conclusion-degree. Our algorithms rely on a sequential approach leveraging from acyclicity, combined with the solution graph traversal technique for the case of premise-degree. They are shown to perform in incremental-polynomial time. These results are complemented in the long version of this document by showing that the dual problem of constructing the implicational base can be solved in polynomial time. Finally, we argue that our running times cannot be improved to polynomial delay using the standard framework of flashlight search.
Cite as

Oscar Defrain, Arthur Ohana, and Simon Vilmin. Enumerating the Irreducible Closed Sets of an Acyclic Implicational Base of Bounded Degree. In 36th International Symposium on Algorithms and Computation (ISAAC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 359, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{defrain_et_al:LIPIcs.ISAAC.2025.24,
  author =	{Defrain, Oscar and Ohana, Arthur and Vilmin, Simon},
  title =	{{Enumerating the Irreducible Closed Sets of an Acyclic Implicational Base of Bounded Degree}},
  booktitle =	{36th International Symposium on Algorithms and Computation (ISAAC 2025)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-408-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{359},
  editor =	{Chen, Ho-Lin and Hon, Wing-Kai and Tsai, Meng-Tsung},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2025.24},
  URN =		{urn:nbn:de:0030-drops-249321},
  doi =		{10.4230/LIPIcs.ISAAC.2025.24},
  annote =	{Keywords: Algorithmic enumeration, closure systems, acyclic convex geometries, solution graph traversal, flashlight search, extension, hypergraph dualization}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.69
A Dichotomy Theorem for Ordinal Ranks in MSO

Authors: Damian Niwiński, Paweł Parys, and Michał Skrzypczak

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We focus on formulae ∃X.φ(Y, X) of monadic second-order logic over the full binary tree, such that the witness X is a well-founded set. The ordinal rank rank(X) < ω₁ of such a set X measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula φ. Let η_φ be the minimal ordinal such that, whenever an instance Y satisfies the formula, there is a witness X with rank(X) ≤ η_φ. Then η_φ is either strictly smaller than ω² or it reaches the maximal possible value ω₁. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.
Cite as

Damian Niwiński, Paweł Parys, and Michał Skrzypczak. A Dichotomy Theorem for Ordinal Ranks in MSO. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 69:1-69:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{niwinski_et_al:LIPIcs.STACS.2025.69,
  author =	{Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{A Dichotomy Theorem for Ordinal Ranks in MSO}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{69:1--69:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.69},
  URN =		{urn:nbn:de:0030-drops-228942},
  doi =		{10.4230/LIPIcs.STACS.2025.69},
  annote =	{Keywords: dichotomy result, limit ordinal, countable ordinals, nondeterministic tree automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.18
Frobenius Structures in Star-Autonomous Categories

Authors: Cédric de Lacroix and Luigi Santocanale

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
It is known that the quantale of sup-preserving maps from a complete lattice to itself is a Frobenius quantale if and only if the lattice is completely distributive. Since completely distributive lattices are the nuclear objects in the autonomous category of complete lattices and sup-preserving maps, we study the above statement in a categorical setting. We introduce the notion of Frobenius structure in an arbitrary autonomous category, generalizing that of Frobenius quantale. We prove that the monoid of endomorphisms of a nuclear object has a Frobenius structure. If the environment category is star-autonomous and has epi-mono factorizations, a variant of this theorem allows to develop an abstract phase semantics and to generalise the previous statement. Conversely, we argue that, in a star-autonomous category where the monoidal unit is a dualizing object, if the monoid of endomorphisms of an object has a Frobenius structure and the monoidal unit embeds into this object as a retract, then the object is nuclear.
Cite as

Cédric de Lacroix and Luigi Santocanale. Frobenius Structures in Star-Autonomous Categories. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{delacroix_et_al:LIPIcs.CSL.2023.18,
  author =	{de Lacroix, C\'{e}dric and Santocanale, Luigi},
  title =	{{Frobenius Structures in Star-Autonomous Categories}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.18},
  URN =		{urn:nbn:de:0030-drops-174798},
  doi =		{10.4230/LIPIcs.CSL.2023.18},
  annote =	{Keywords: Quantale, Frobenius quantale, Girard quantale, associative algebra, star-autonomous category, nuclear object, adjoint}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.38
Aleph1 and the Modal mu-Calculus

Authors: Maria João Gouveia and Luigi Santocanale

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
For a regular cardinal kappa, a formula of the modal mu-calculus is kappa-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of kappa-directed sets. We define the fragment C1 (x) of the modal mu-calculus and prove that all the formulas in this fragment are aleph_1-continuous. For each formula phi(x) of the modal mu-calculus, we construct a formula psi(x) in C1 (x) such that phi(x) is kappa-continuous, for some kappa, if and only if psi(x) is equivalent to phi(x). Consequently, we prove that (i) the problem whether a formula is kappa-continuous for some kappa is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C0(x) studied by Fontaine and the fragment C1 (x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal mu-calculus. An ordinal alpha is the closure ordinal of a formula phi(x) if its interpretation on every model converges to its least fixed-point in at most alpha steps and if there is a model where the convergence occurs exactly in alpha steps. We prove that omega_1, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, omega, omega_1 by using the binary operator symbol + gives rise to a closure ordinal.
Cite as

Maria João Gouveia and Luigi Santocanale. Aleph1 and the Modal mu-Calculus. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gouveia_et_al:LIPIcs.CSL.2017.38,
  author =	{Gouveia, Maria Jo\~{a}o and Santocanale, Luigi},
  title =	{{Aleph1 and the Modal mu-Calculus}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.38},
  URN =		{urn:nbn:de:0030-drops-76926},
  doi =		{10.4230/LIPIcs.CSL.2017.38},
  annote =	{Keywords: Modal mu-calculus, regular cardinal, continuous function, aleph1, omega1, closure ordinal, ordinal sum}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.248
Cuts for circular proofs: semantics and cut-elimination

Authors: Jérôme Fortier and Luigi Santocanale

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
One of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]). In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.
Cite as

Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 248-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fortier_et_al:LIPIcs.CSL.2013.248,
  author =	{Fortier, J\'{e}r\^{o}me and Santocanale, Luigi},
  title =	{{Cuts for circular proofs: semantics and cut-elimination}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{248--262},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.248},
  URN =		{urn:nbn:de:0030-drops-42019},
  doi =		{10.4230/LIPIcs.CSL.2013.248},
  annote =	{Keywords: categorical proof-theory, fixpoints, initial and final (co)algebras, inductive and coinductive types}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2023
  • 1 2017
  • 1 2013

  • Refine by Author
  • 3 Santocanale, Luigi
  • 1 Defrain, Oscar
  • 1 Fortier, Jérôme
  • 1 Gouveia, Maria João
  • 1 Niwiński, Damian
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 1 Mathematics of computing → Enumeration
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 1 Algorithmic enumeration
  • 1 Frobenius quantale
  • 1 Girard quantale
  • 1 Modal mu-calculus
  • 1 Quantale
  • 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