Abstract
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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Ainouche, A.: Quasi-claw-free graphs. Discrete Math. 179(1–3), 13–26 (1998)
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)
Bang-Jensen, J., Gutin, G.: Digraphs Theory, Algorithms and Applications, 1st edn. Springer, Berlin (2000)
Beineke, L.: Beiträge zur Graphentheorie, chap. Derived graphs and digraphs. Teubner, Leipzig (1968)
Beineke, L.: Characterizations of derived graphs. J. Comb. Theory, Ser. B 9, 129–135 (1970)
Belinfante, J.G.F.: On a modification of Gödel’s algorithm for class formation. AAR Newsletter 34, 10–15 (1996)
Belinfante, J.G.F.: On computer-assisted proofs in ordinal number theory. J. Autom. Reason. 22(2), 341–378 (1999)
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)
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)
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)
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)
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)
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)
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)
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)
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)
Chudnovsky, M., Robertson, N., Seymour, P., Thomas, R.: The strong perfect graph theorem. Ann. Math. 164(1), 51–229 (2006)
Chudnovsky, M., Seymour, P.D.: Claw-free graphs. I. Orientable prismatic graphs. J. Comb. Theory, Ser. B 97(6), 867–903 (2007)
Chudnovsky, M., Seymour, P.D.: Claw-free graphs. VI. Colouring. J. Comb. Theory, Ser. B 100(6), 560–572 (2010)
Eaton, N., Grable, D.A.: Set intersection representations for almost all graphs. J. Graph Theory 23(3), 309–320 (1996)
Faudree, R., Flandrin, E., Ryjáček, Z.: Claw-flee graphs—a survey. Discrete Math. 164, 87–147 (1997)
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)
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)
Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer Berlin/Heidelberg (2005)
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)
Golumbic, M.C.: Interval graphs and related topics. Discrete Math. 55(2), 113–121 (1985)
Golumbic, M.C.: Algorithmic aspects of intersection graphs and representation hypergraphs. Graphs Comb. 4(1), 307–321 (1988)
Gonthier, G.: Formal proof—the four-color theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)
Hendry, G., Vogler, W.: The square of a connected S(K 1,3)-free graph is vertex pancyclic. J. Graph Theory 9(4), 535–537 (1985)
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)
Levy, A.: Basic Set Theory. Springer, Berlin (1979)
Matthews, M.M., Sumner, D.P.: Hamiltonian Results in K 1,3-Free Graphs. J. Graph Theory 8, 139–146 (1984)
Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and its Applications 4(1), 3–24 (2005)
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
Moore, J.S., Zhang, Q.: Proof pearl: Dijkstra’s shortest path algorithm verified with ACL2. In: Proceedings of the 18th international conference on Theorem Proving in Higher Order Logics, TPHOLs’05, pp. 373–384. Springer-Verlag, Berlin, Heidelberg (2005)
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
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)
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)
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)
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)
Parthasarathy, K.R., Ravindra, G.: The strong perfect-graph conjecture is true for K 1,3-free graphs. J. Combin. Theory, Ser. B 21(3), 212–223 (1976)
Quaife, A.: Automated deduction in von Neumann-Bernays-Gödel set theory. J. Automat. Reason. 8(1), 91–147 (1992)
Ryjáček, Z.: Almost claw-free graphs. J. Graph Theory 18(5), 469–477 (1994)
Schwartz, J.T., Cantone, D., Omodeo, E.G.: Computational Logic and Set Theory. Springer (2011). Foreword by Martin Davis
Sumner, D.: Graphs with 1-factors. Proc. Amer. Math. Soc. 42, 8–12 (1974)
Szpilrajn-Marczewski, E.: Sur deux propriétés des classes d’ensemble. Fund. Math. 33, 303–307 (1945)
Tarski, A.: Sur les ensembles fini. Fund. Math. VI, 45–95 (1924)
Tarski, A., Givant, S.: A formalization of set theory without variables. In: Colloquium Publications, vol. 41. American Mathematical Society (1987)
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)
Vergnas, M.L.: A note on matchings in graphs. Cahiers Centre Etudes Rech. Opér. 17, 257–260 (1975)
Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3–4), 389–411 (2002)
Wiedijk, F.: Mizar: An impression. http://www.cs.ru.nl/~freek/mizar/mizarintro.ps.gz (1999). Accessed 1 April 2012
Wos, L.: The problem of finding an inference rule for set theory. J. Autom. Reason. 5(1), 93–95 (1989)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Omodeo, E.G., Tomescu, A.I. Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets. J Autom Reasoning 52, 1–29 (2014). https://doi.org/10.1007/s10817-012-9272-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-012-9272-3