Top

Journal of Automated Reasoning

Published in:

31-01-2020

Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

Authors: Christian Doczkal, Damien Pous

Published in: Journal of Automated Reasoning | Issue 5/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Preface: Selected Extended Papers from Interactive Theorem Proving 2018

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

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

To be fully precise, we use the type \(\varSigma x:G.\,x \in U = \textsf {true}\), exploiting that set membership is decidable. Since equality between booleans is proof irrelevant (i.e., there is at most one proof of \(x \in U = \textsf {true}\)), this ensures that \(\left| (G|_U)\right| = |\varSigma x:G.\,x \in U| = |U|\). This is a standard technique used pervasively in the mathematical components library.

Note that \(\overline{V_2} = V_1 \setminus V_2\) if \( V_1 \cup V_2 = V\).

To be precise, the functional may call its argument on anything. However, the result may only depend on calls to smaller arguments in the domain.

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 FrenchCrossRef

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
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 5/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-020-09543-2

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 5/2020

Verified Analysis of Random Binary Tree Structures

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

Preface: Selected Extended Papers from Interactive Theorem Proving 2018

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

The MetaCoq Project

Formal Reasoning Under Cached Address Translation

Premium Partner