3 Search Results for "Doczkal, Christian"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.135
A Finite Presentation of Graphs of Treewidth at Most Three

Authors: Amina Doumane, Samuel Humeau, and Damien Pous

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We provide a finite equational presentation of graphs of treewidth at most three, solving an instance of an open problem by Courcelle and Engelfriet. We use a syntax generalising series-parallel expressions, denoting graphs with a small interface. We introduce appropriate notions of connectivity for such graphs (components, cutvertices, separation pairs). We use those concepts to analyse the structure of graphs of treewidth at most three, showing how they can be decomposed recursively, first canonically into connected parallel components, and then non-deterministically. The main difficulty consists in showing that all non-deterministic choices can be related using only finitely many equational axioms.
Cite as

Amina Doumane, Samuel Humeau, and Damien Pous. A Finite Presentation of Graphs of Treewidth at Most Three. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 135:1-135:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{doumane_et_al:LIPIcs.ICALP.2024.135,
  author =	{Doumane, Amina and Humeau, Samuel and Pous, Damien},
  title =	{{A Finite Presentation of Graphs of Treewidth at Most Three}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{135:1--135:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.135},
  URN =		{urn:nbn:de:0030-drops-202787},
  doi =		{10.4230/LIPIcs.ICALP.2024.135},
  annote =	{Keywords: Graphs, treewidth, connectedness, axiomatisation, series-parallel expressions}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.17
A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps

Authors: Christian Doczkal

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
Wagner’s theorem states that a graph is planar (i.e., it can be embedded in the real plane without crossing edges) iff it contains neither 𝖪_5 nor 𝖪_{3,3} as a minor. We provide a combinatorial representation of embeddings in the plane that abstracts from topological properties of plane embeddings (e.g., angles or distances), representing only the combinatorial properties (e.g., arities of faces or the clockwise order of the outgoing edges of a vertex). The representation employs combinatorial hypermaps as used by Gonthier in the proof of the four-color theorem. We then give a formal proof that for every simple graph containing neither 𝖪_5 nor 𝖪_{3,3} as a minor, there exists such a combinatorial plane embedding. Together with the formal proof of the four-color theorem, we obtain a formal proof that all graphs without 𝖪_5 and 𝖪_{3,3} minors are four-colorable. The development is carried out in Coq, building on the mathematical components library, the formal proof of the four-color theorem, and a general-purpose graph library developed previously.
Cite as

Christian Doczkal. A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doczkal:LIPIcs.ITP.2021.17,
  author =	{Doczkal, Christian},
  title =	{{A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.17},
  URN =		{urn:nbn:de:0030-drops-139123},
  doi =		{10.4230/LIPIcs.ITP.2021.17},
  annote =	{Keywords: Coq, MathComp, Graph-Theory, Hypermaps, Planarity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.60
Treewidth-Two Graphs as a Free Algebra

Authors: Christian Doczkal and Damien Pous

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We give a new and elementary proof that the graphs of treewidth at most two can be seen as a free algebra. This result was originally established through an elaborate analysis of the structure of K_4-free graphs, ultimately reproving the well-known fact that the graphs of treewidth at most two are precisely those excluding K_4 as a minor. Our new proof is based on a confluent and terminating rewriting system for term-labeled graphs and does not involve graph minors anymore. The new strategy is simpler and robust in the sense that it can be adapted to subclasses of treewidth-two graphs, e.g., graphs without self-loops.
Cite as

Christian Doczkal and Damien Pous. Treewidth-Two Graphs as a Free Algebra. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 60:1-60:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doczkal_et_al:LIPIcs.MFCS.2018.60,
  author =	{Doczkal, Christian and Pous, Damien},
  title =	{{Treewidth-Two Graphs as a Free Algebra}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{60:1--60:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.60},
  URN =		{urn:nbn:de:0030-drops-96429},
  doi =		{10.4230/LIPIcs.MFCS.2018.60},
  annote =	{Keywords: Treewidth, Universal Algebra, Rewriting}
}
  • Refine by Author
  • 2 Doczkal, Christian
  • 2 Pous, Damien
  • 1 Doumane, Amina
  • 1 Humeau, Samuel

  • Refine by Classification
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Mathematics of computing → Graph theory
  • 1 Mathematics of computing → Graphs and surfaces
  • 1 Mathematics of computing → Paths and connectivity problems
  • 1 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 1 Coq
  • 1 Graph-Theory
  • 1 Graphs
  • 1 Hypermaps
  • 1 MathComp
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2018
  • 1 2021
  • 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