Top

previous article Preface: Selected Extended Papers from Interact...

next article Formalizing the LLL Basis Reduction Algorithm a...

Hint

Swipe to navigate through the articles of this issue

31-01-2020 | Issue 5/2020

Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

Journal:: Journal of Automated Reasoning > Issue 5/2020

Authors:: Christian Doczkal, Damien Pous

» Get access to the full-text

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.

inform now

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.

inform now

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.

inform now

Chekuri, C., Rajaraman, A.: Conjunctive query containment revisited. Theoret. Comput. Sci. 239(2), 211–229 (2000). https://doi.org/10.1016/S0304-3975(99)00220-0 MathSciNetCrossRefMATH

Chou, C.: A formal theory of undirected graphs in higher-order logic. In: Melham, T.F., Camilleri, J. (eds.) TPHOL, Lecture Notes in Computer Science, vol. 859, pp. 144–157. Springer (1994). https://doi.org/10.1007/3-540-58450-1_40

Chou, C.T.: Mechanical verification of distributed algorithms in higher-order logic*. Comput. J. 38(2), 152–161 (1995). https://doi.org/10.1093/comjnl/38.2.152 CrossRef

Cohen, C.: Pragmatic quotient types in Coq. In: In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP, Lecture Notes in Computer Science, vol. 7998, pp. 213–228. Springer (2013). https://doi.org/10.1007/978-3-642-39634-2_17

Cohen, C., Dénès, M., Mörtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs (CPP 2013), Lecture Notes in Computer Science, vol. 8307, pp. 147–162. Springer, Berlin (2013). https://doi.org/10.1007/978-3-319-03545-1_10 CrossRef

Courcelle, B.: The monadic second-order logic of graphs. I: recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990). https://doi.org/10.1016/0890-5401(90)90043-H MathSciNetCrossRefMATH

Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic—A Language-Theoretic Approach, Encyclopedia of Mathematics and Its Applications, vol. 138. Cambridge University Press, Cambridge (2012) MATH

Diestel, R.: Graph Theory. Graduate Texts in Mathematics, 2nd edn. Springer, Berlin (2000)

Doczkal, C., Combette, G., Pous, D.: Coq Formalization Accompanying This Paper. https://perso.ens-lyon.fr/damien.pous/covece/graphs/. Accessed 28 Jan 2020

10.

Doczkal, C., Combette, G., Pous, D.: A formal proof of the minor-exclusion property for treewidth-two graphs. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving (ITP 2018), Lecture Notes in Computer Science, vol. 10895, pp. 178–195. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-94821-8_11 CrossRef

11.

Doczkal, C., Pous, D.: Treewidth-two graphs as a free algebra. In: Potapov, I, Spirakis, P., Worrell, J. (eds.) MFCS, LIPIcs, vol. 117, pp. 60:1–60:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPIcs.MFCS.2018.60

12.

Doczkal, C., Pous, D.: Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. In: Proceedings of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20–21, 2020, New Orleans, LA, USA (2020). https://doi.org/10.1145/3372885.3373831

13.

Duffin, R.: Topology of series-parallel networks. J. Math. Anal. Appl. 10(2), 303–318 (1965). https://doi.org/10.1016/0022-247X(65)90125-3 MathSciNetCrossRefMATH

14.

Dufourd, J., Bertot, Y.: Formal study of plane Delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP, Lecture Notes in Computer Science, vol. 6172, pp. 211–226. Springer (2010). https://doi.org/10.1007/978-3-642-14052-5_16

15.

Freuder, E.C.: Complexity of k-tree structured constraint satisfaction problems. In: Shrobe, H.E., Dietterich, T.G., Swartout, W.R. (eds.) NCAI, pp. 4–9. AAAI Press/The MIT Press (1990)

16.

Freyd, P., Scedrov, A.: Categories, Allegories. Elsevier, North Holland (1990) MATH

17.

Gonthier, G.: Formal proof—the four-color theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008) MathSciNetMATH

18.

Göring, F.: Short proof of menger’s theorem. Discrete Math. 219(1–3), 295–296 (2000). https://doi.org/10.1016/S0012-365X(00)00088-1 MathSciNetCrossRefMATH

19.

Grohe, M.: The complexity of homomorphism and constraint satisfaction problems seen from the other side. J. ACM 54(1), 1:1–1:24 (2007). https://doi.org/10.1145/1206035.1206036 MathSciNetCrossRefMATH

20.

Hall, P.: On representatives of subsets. J. Lond. Math. Soc. 10, 26–30 (1935). https://doi.org/10.1112/jlms/s1-10.37.26 CrossRefMATH

21.

Kuratowski, K.: Sur le problème des courbes gauches en topologie. Fund. Math. 15, 271–283 (1930). In French CrossRef

22.

Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds–Karp algorithm. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science, vol. 9807, pp. 219–234. Springer, Berlin (2016). https://doi.org/10.1007/978-3-319-43144-4_14 CrossRef

23.

Llópez, E.C., Pous, D.: K4-free graphs as a free algebra. In: Larsen, K.G., Bodlaender, H.L., Raskin, J-F. (eds.) MFCS, LIPIcs, vol. 83, pp. 76:1–76:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPIcs.MFCS.2017.76

24.

Menger, K.: Zur allgemeinen Kurventheorie. Fund. Math. 10(1), 96–115 (1927) CrossRef

25.

Nakamura, Y., Rudnicki, P.: Euler circuits and paths. Formal. Math. 6(3), 417–425 (1997)

26.

Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: tame graphs. In: Furbach U., Shankar N. (eds.) IJCAR, Lecture Notes in Computer Science, vol. 4130, pp. 21–35. Springer (2006). https://doi.org/10.1007/11814771_4

27.

Noschinski, L.: A graph library for Isabelle. Math. Comput. Sci. 9(1), 23–39 (2015). https://doi.org/10.1007/s11786-014-0183-z MathSciNetCrossRefMATH

28.

Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction (CADE-25), Lecture Notes in Computer Science, vol. 9195, pp. 231–245. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-21401-6_15 CrossRef

29.

Pous, D., Vignudelli, V.: Allegories: decidability and graph homomorphisms. In: Dawar, A., Grädel, E. (eds.) LiCS, pp. 829–838. ACM (2018). https://doi.org/10.1145/3209108.3209172

30.

Robertson, N., Seymour, P.: Graph minors. XX. Wagner’s conjecture. J. Comb. Theory Ser. B 92(2), 325–357 (2004). https://doi.org/10.1016/j.jctb.2004.08.001 MathSciNetCrossRefMATH

31.

Severín, D.E.: Formalization of the domination chain with weighted parameters (short paper). In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) Interactive Theorem Provin (ITP 2019), LIPIcs, vol. 141, pp. 36:1–36:7. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Wadern (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.36 CrossRef

32.

Singh, A.K., Natarajan, R.: A constructive formalization of the weak perfect graph theorem. In: Proceedings of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20–21, 2020, New Orleans, LA, USA (2020)

33.

Sozeau, M.: A new look at generalized rewriting in type theory. J. Formaliz. Reason. 2(1), 41–62 (2009). https://doi.org/10.6092/issn.1972-5787/1574 MathSciNetCrossRefMATH

34.

The Mathematical Components team: Mathematical components (2017). http://math-comp.github.io/math-comp/. Accessed 28 Jan 2020

35.

Univalent Foundations Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study (2013)

Title: Graph Theory in Coq: Minors, Treewidth, and Isomorphisms
Authors:: Christian Doczkal
Damien Pous
Publication date: 31-01-2020
DOI: https://doi.org/10.1007/s10817-020-09543-2
Publisher: Springer Netherlands
Journal: Journal of Automated Reasoning
Issue 5/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670

Premium Partner

Image Credits

Springer Professional

Hint

Swipe to navigate through the articles of this issue

Publisher's Note

Abstract

Please log in to get access to this content

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 5/2020

The MetaCoq Project

Formal Reasoning Under Cached Address Translation

Verified Analysis of Random Binary Tree Structures

Preface: Selected Extended Papers from Interactive Theorem Proving 2018

A Relaxation of Üresin and Dubois’ Asynchronous Fixed-Point Theory in Agda

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

Premium Partner