Search Results

Documents authored by Grange, Julien

Document
DOI: 10.4230/LIPIcs.MFCS.2024.56
Specification and Automatic Verification of Computational Reductions

Authors: Julien Grange, Fabian Vehlken, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
We are interested in the following validation problem for computational reductions: for algorithmic problems P and P^⋆, is a given candidate reduction indeed a reduction from P to P^⋆? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation problem can be attacked algorithmically? We answer this question positively by introducing an easy-to-use graphical specification mechanism for computational reductions, called cookbook reductions. We show that cookbook reductions are sufficiently expressive to cover many classical graph reductions and expressive enough so that SAT remains NP-complete (in the presence of a linear order). Surprisingly, the validation problem is decidable for natural and expressive subclasses of cookbook reductions.
Cite as

Julien Grange, Fabian Vehlken, Nils Vortmeier, and Thomas Zeume. Specification and Automatic Verification of Computational Reductions. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 56:1-56:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{grange_et_al:LIPIcs.MFCS.2024.56,
  author =	{Grange, Julien and Vehlken, Fabian and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Specification and Automatic Verification of Computational Reductions}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{56:1--56:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.56},
  URN =		{urn:nbn:de:0030-drops-206122},
  doi =		{10.4230/LIPIcs.MFCS.2024.56},
  annote =	{Keywords: Computational reductions, automatic verification, decidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.23
Order-Invariance in the Two-Variable Fragment of First-Order Logic

Authors: Julien Grange

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

Abstract
We study the expressive power of the two-variable fragment of order-invariant first-order logic. This logic departs from first-order logic in two ways: first, formulas are only allowed to quantify over two variables. Second, formulas can use an additional binary relation, which is interpreted in the structures under scrutiny as a linear order, provided that the truth value of a sentence over a finite structure never depends on which linear order is chosen on its domain. We prove that on classes of structures of bounded degree, any property expressible in this logic is definable in first-order logic. We then show that the situation remains the same when we add counting quantifiers to this logic.
Cite as

Julien Grange. Order-Invariance in the Two-Variable Fragment of First-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{grange:LIPIcs.CSL.2023.23,
  author =	{Grange, Julien},
  title =	{{Order-Invariance in the Two-Variable Fragment of First-Order Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{23:1--23:19},
  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.23},
  URN =		{urn:nbn:de:0030-drops-174846},
  doi =		{10.4230/LIPIcs.CSL.2023.23},
  annote =	{Keywords: Finite model theory, Two-variable logic, Order-invariance}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.23
Order-Invariant First-Order Logic over Hollow Trees

Authors: Julien Grange and Luc Segoufin

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

Abstract
We show that the expressive power of order-invariant first-order logic collapses to first-order logic over hollow trees. A hollow tree is an unranked ordered tree where every non leaf node has at most four adjacent nodes: two siblings (left and right) and its first and last children. In particular there is no predicate for the linear order among siblings nor for the descendant relation. Moreover only the first and last nodes of a siblinghood are linked to their parent node, and the parent-child relation cannot be completely reconstructed in first-order.
Cite as

Julien Grange and Luc Segoufin. Order-Invariant First-Order Logic over Hollow Trees. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{grange_et_al:LIPIcs.CSL.2020.23,
  author =	{Grange, Julien and Segoufin, Luc},
  title =	{{Order-Invariant First-Order Logic over Hollow Trees}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{23:1--23: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.23},
  URN =		{urn:nbn:de:0030-drops-116661},
  doi =		{10.4230/LIPIcs.CSL.2020.23},
  annote =	{Keywords: order-invariance, first-order logic}
}
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 About DROPS Imprint Privacy Contact