Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

31-01-2020 | Issue 5/2020

Journal of Automated Reasoning 5/2020

Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

Journal:
Journal of Automated Reasoning > Issue 5/2020
Authors:
Christian Doczkal, Damien Pous
Important notes
This paper extends and revises the results presented in [10]; the underlying Coq library is available from https://​perso.​ens-lyon.​fr/​damien.​pous/​covece/​graphs/​.
This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, Grant Agreement No. 678157), and was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon and \(\hbox {UCA}^{\text {JEDI}}\), within the programs “Investissements d’Avenir” ANR-11-IDEX-0007 and ANR-15-IDEX-01, respectively.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalize several results from the literature: Menger’s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe




Testen Sie jetzt 30 Tage kostenlos.

Literature
About this article

Other articles of this Issue 5/2020

Journal of Automated Reasoning 5/2020 Go to the issue

OriginalPaper

The MetaCoq Project

Premium Partner

    Image Credits