×

Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets. (English) Zbl 1315.68223

Summary: We report on the formalization of two classical results about claw-free graphs, which have been verified correct by Jacob T. Schwartz’s proof-checker Referee. We have proved formally that every connected claw-free graph admits (1) a near-perfect matching, (2) Hamiltonian cycles in its square. To take advantage of the set-theoretic foundation of Referee, we exploited set equivalents of the graph-theoretic notions involved in our experiment: edge, source, square, etc. To ease some proofs, we have often resorted to weak counterparts of well-established notions such as cycle, claw-freeness, longest directed path, etc.
For Part II see [M. Milanič et al., Theor. Comput. Sci. 547, 70–81 (2014; Zbl 1298.05146)].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
05C75 Structural characterization of families of graphs

Citations:

Zbl 1298.05146
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ainouche, A.: Quasi-claw-free graphs. Discrete Math. 179(1-3), 13-26 (1998) · Zbl 0888.05038 · doi:10.1016/S0012-365X(97)00023-X
[2] Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C.: Verification of certifying computations. In: Gopalakrishnan, G., Qadeer, S., (eds.) CAV, Lecture Notes in Computer Science, vol. 6806, pp. 67-82. Springer (2011) · Zbl 1314.68180
[3] Bang-Jensen, J., Gutin, G.: Digraphs Theory, Algorithms and Applications, 1st edn. Springer, Berlin (2000) · Zbl 0958.05002
[4] Beineke, L.: Beiträge zur Graphentheorie, chap. Derived graphs and digraphs. Teubner, Leipzig (1968)
[5] Beineke, L.: Characterizations of derived graphs. J. Comb. Theory, Ser. B 9, 129-135 (1970) · Zbl 0202.55702 · doi:10.1016/S0021-9800(70)80019-9
[6] Belinfante, J.G.F.: On a modification of Gödel’s algorithm for class formation. AAR Newsletter 34, 10-15 (1996)
[7] Belinfante, J.G.F.: On computer-assisted proofs in ordinal number theory. J. Autom. Reason. 22(2), 341-378 (1999) · Zbl 0922.68111 · doi:10.1023/A:1006010913494
[8] Belinfante, J.G.F.: Gödel’s algorithm for class formation. In: McAllester, D.A. (ed.) CADE, Lecture Notes in Computer Science, vol. 1831, pp. 132-147. Springer (2000) · Zbl 0963.68183
[9] Belinfante, J.G.F.: Computer proofs about finite and regular sets: the unifying concept of subvariance. J. Symb. Comput. 36(1-2), 271-285 (2003) · Zbl 1039.68115 · doi:10.1016/S0747-7171(03)00023-3
[10] Belinfante, J.G.F.: Reasoning about iteration in Gödel’s class theory. In: Baader, F. (ed.) CADE, Lecture Notes in Computer Science, vol. 2741, pp. 228-242. Springer (2003) · Zbl 1260.68365
[11] Berge, C.: Färbung von Graphen, deren sämtliche bzw. deren ungerade Kreise starr sind. Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10, 114 (1961)
[12] Boyer, R.S., Lusk, E.L., McCune, W., Overbeek, R.A., Stickel, M.E., Wos, L.: Set theory in first-order logic: Clauses for Gödel’s axioms. J. Autom. Reason. 2(3), 287-327 (1986) · Zbl 0635.03008 · doi:10.1007/BF02328452
[13] Brandstädt, A., Le, V.B., Spinrad, J.P.: Graph Classes: A Survey, Monographs on Discrete Mathematics and Applications, vol. 3. SIAM Society for Industrial and Applied Mathematics, Philadelphia (1999) · Zbl 0919.05001 · doi:10.1137/1.9780898719796
[14] Brown, C.E.: Combining type theory and untyped set theory. In: Furbach, U., Shankar, N. (eds.) IJCAR, Lecture Notes in Computer Science, vol. 4130, pp. 205-219. Springer (2006) · Zbl 1222.03012
[15] Burstall, R., Goguen, J.: Putting theories together to make specifications. In: Reddy, R. (ed.) Proc. 5th International Joint Conference on Artificial Intelligence, pp. 1045-1058. Cambridge, MA (1977) · Zbl 1195.05026
[16] Cantone, D., Omodeo, E.G., Schwartz, J.T., Ursino, P.: Notes from the logbook of a proof-checker’s project. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, Lecture Notes in Computer Science, vol. 2772, pp. 182-207. Springer (2003) · Zbl 1274.68407
[17] Chudnovsky, M., Robertson, N., Seymour, P., Thomas, R.: The strong perfect graph theorem. Ann. Math. 164(1), 51-229 (2006) · Zbl 1112.05042 · doi:10.4007/annals.2006.164.51
[18] Chudnovsky, M., Seymour, P.D.: Claw-free graphs. I. Orientable prismatic graphs. J. Comb. Theory, Ser. B 97(6), 867-903 (2007) · Zbl 1128.05031 · doi:10.1016/j.jctb.2007.02.002
[19] Chudnovsky, M., Seymour, P.D.: Claw-free graphs. VI. Colouring. J. Comb. Theory, Ser. B 100(6), 560-572 (2010) · Zbl 1207.05050 · doi:10.1016/j.jctb.2010.04.005
[20] Eaton, N., Grable, D.A.: Set intersection representations for almost all graphs. J. Graph Theory 23(3), 309-320 (1996) · Zbl 0948.05036 · doi:10.1002/(SICI)1097-0118(199611)23:3<309::AID-JGT11>3.0.CO;2-9
[21] Faudree, R., Flandrin, E., Ryjáček, Z.: Claw-flee graphs—a survey. Discrete Math. 164, 87-147 (1997) · Zbl 0879.05043 · doi:10.1016/S0012-365X(96)00045-3
[22] Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Commun. Pure Appl. Math. 33(5), 599-608 (1980) · Zbl 0453.03009 · doi:10.1002/cpa.3160330503
[23] Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for some fragments of set theory. In: Bibel, W., Kowalski, R. (eds.) Proc. 5th Conference on Automated Deduction, LNCS, vol. 87, pp. 88-96. Springer-Verlag (1980) · Zbl 0457.03009
[24] Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer Berlin/Heidelberg (2005) · Zbl 1142.68032
[25] Formisano, A., Omodeo, E.G.: Theory-specific automated reasoning. In: Dovier, A., Pontelli, E. (eds.) A 25-Year Perspective on Logic Programming: Achievements of the Italian Association for Logic Programming, GULP, Lecture Notes in Computer Science, vol. 6125, pp. 37-63. Springer (2010) · Zbl 1285.68146
[26] Golumbic, M.C.: Interval graphs and related topics. Discrete Math. 55(2), 113-121 (1985) · Zbl 0568.05046 · doi:10.1016/0012-365X(85)90039-1
[27] Golumbic, M.C.: Algorithmic aspects of intersection graphs and representation hypergraphs. Graphs Comb. 4(1), 307-321 (1988) · Zbl 0671.05034 · doi:10.1007/BF01864170
[28] Gonthier, G.: Formal proof—the four-color theorem. Not. Am. Math. Soc. 55(11), 1382-1393 (2008) · Zbl 1195.05026
[29] Hendry, G., Vogler, W.: The square of a connected S(K1,3)-free graph is vertex pancyclic. J. Graph Theory 9(4), 535-537 (1985) · Zbl 0664.05038 · doi:10.1002/jgt.3190090415
[30] Jünger, M., Reinelt, G., Pulleyblank, W.R.: On partitioning the edges of graphs into connected subgraphs. J. Graph Theory 9(4), 539-549 (1985) · Zbl 0665.05040 · doi:10.1002/jgt.3190090416
[31] Levy, A.: Basic Set Theory. Springer, Berlin (1979) · Zbl 0404.04001 · doi:10.1007/978-3-662-02308-2
[32] Matthews, M.M., Sumner, D.P.: Hamiltonian Results in K1,3-Free Graphs. J. Graph Theory 8, 139-146 (1984) · Zbl 0536.05047 · doi:10.1002/jgt.3190080116
[33] Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and its Applications 4(1), 3-24 (2005)
[34] Milanič, M., Tomescu, A.I.: Set graphs. I. Hereditarily finite sets and extensional acyclic orientations. Discrete Appl. Math. (2011). doi:10.1016/j.dam.2011.11.027 · Zbl 1259.05143 · doi:10.1016/j.dam.2011.11.027
[35] Moore, JS; Zhang, Q., Proof pearl: Dijkstra’s shortest path algorithm verified with ACL2, 373-384 (2005), Berlin, Heidelberg · Zbl 1152.68526 · doi:10.1007/11541868_24
[36] Nordhoff, B., Lammich, P.: Dijkstra’s shortest path algorithm. Archive of Formal Proofs (2012). http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml, Formal proof development · Zbl 1112.05042
[37] Omodeo, E.G.: The Ref proof-checker and its “common shared scenario”. In: Davis, M., Schonberg, E. (eds.) From Linear Operators to Computational Biology: Essays in Memory of Jacob T. Schwartz, pp. 121-131. Springer (2012)
[38] Omodeo, E.G., Cantone, D., Policriti, A., Schwartz, J.T.: A Computerized Referee. In: Stock, O., Schaerf, M. (eds.) Reasoning, Action and Interaction in AI Theories and Systems—Essays Dedicated to Luigia Carlucci Aiello, LNAI, vol. 4155, pp. 117-139. Springer (2006)
[39] Omodeo, E.G., Schwartz, J.T.: A ‘theory’ mechanism for a proof-verifier based on first-order set theory. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II, Lecture Notes in Computer Science, vol. 2408, pp. 214-230. Springer (2002) · Zbl 1012.68181
[40] Omodeo, E.G., Tomescu, A.I.: Appendix: claw-free graphs as sets. In: Davis, M., Schonberg, E. (eds.) From Linear Operators to Computational Biology: Essays in Memory of Jacob T. Schwartz, pp. 131-167. Springer (2012) · Zbl 0315.05123
[41] Parthasarathy, K.R., Ravindra, G.: The strong perfect-graph conjecture is true for K1,3-free graphs. J. Combin. Theory, Ser. B 21(3), 212-223 (1976) · Zbl 0297.05109 · doi:10.1016/S0095-8956(76)80005-6
[42] Quaife, A.: Automated deduction in von Neumann-Bernays-Gödel set theory. J. Automat. Reason. 8(1), 91-147 (1992) · Zbl 0768.03005
[43] Ryjáček, Z.: Almost claw-free graphs. J. Graph Theory 18(5), 469-477 (1994) · Zbl 0808.05067 · doi:10.1002/jgt.3190180505
[44] Schwartz, J.T., Cantone, D., Omodeo, E.G.: Computational Logic and Set Theory. Springer (2011). Foreword by Martin Davis · Zbl 1246.03006
[45] Sumner, D.: Graphs with 1-factors. Proc. Amer. Math. Soc. 42, 8-12 (1974) · Zbl 0293.05157
[46] Szpilrajn-Marczewski, E.: Sur deux propriétés des classes d’ensemble. Fund. Math. 33, 303-307 (1945) · Zbl 0060.12508
[47] Tarski, A.: Sur les ensembles fini. Fund. Math. VI, 45-95 (1924)
[48] Tarski, A., Givant, S.: A formalization of set theory without variables. In: Colloquium Publications, vol. 41. American Mathematical Society (1987) · Zbl 0654.03036
[49] Verbeek, F., Schmaltz, J.: Proof pearl: a formal proof of Dally and Seitz’ necessary and sufficient condition for deadlock-free routing in interconnection networks. J. Autom. Reason. 48(4), 419-439 (2012) · Zbl 1242.68284 · doi:10.1007/s10817-010-9206-x
[50] Vergnas, M.L.: A note on matchings in graphs. Cahiers Centre Etudes Rech. Opér. 17, 257-260 (1975) · Zbl 0315.05123
[51] Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3-4), 389-411 (2002) · Zbl 1064.68083 · doi:10.1023/A:1021935419355
[52] Wiedijk, F.: Mizar: An impression. http://www.cs.ru.nl/ freek/mizar/mizarintro.ps.gz (1999). Accessed 1 April 2012
[53] Wos, L.: The problem of finding an inference rule for set theory. J. Autom. Reason. 5(1), 93-95 (1989) · Zbl 0679.68178
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.