Abstract
Modeling a mathematical notion in convenient set-theoretic terms is seldom a trivial task, and formalization inside Set Theory calls for design choices. This chapter will illustrate this, referring to the class of claw-free graphs thoroughly discussed in the previous chapter.We will manage to represent connected claw-free graphs as specially constrained transitive sets: each element x′ of the set T that represents one such graph will act as a corresponding vertex x and the edge relationship will be mimicked by membership over T. That is, either x′ ∈ y′ or y′ ∈ x′ will hold when {x′, y′} ⊆ T is the set corresponding to an edge {x, y} of the original graph. Even though our representation will superimpose an apparently artificial orientation to an undirected graph, we will take advantage precisely of this redundancy to prove with relative ease that every connected claw-free graph has a near-perfect matching and a Hamiltonian cycle in its square.By relying on this representation, we can verify the correctness of the proofs supplied in this chapter with the aid of a programmed proof assistant, Ref. With a more conventional representation of graphs, the size of the formalized proofs would have been discouragingly big for such an experiment; on the opposite, thanks to the representation adopted, the formalized proof turns out to be an affordable ‘proof pearl’.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In its customary wording, this theorem claims that every claw-free connected graph with an even number of vertices has a perfect matching; according to our touched-up rewording, one vertex can be left unmatched—needless to say, this will happen when the number of vertices is odd.
- 2.
This definition covers, along with the notion of graph proper, also the case V = E = ∅.
- 3.
By slightly deviating from the notation employed so far, in this chapter we are conforming to the manner formulae are pretty-printed by our proof checker Ref. For example, we will often write \(\langle \exists x \in t\,\vert \:\varphi \rangle\) instead of \(\exists s \in t\;\varphi\) and will do similarly with universal restricted quantifiers.
- 4.
The “negative solution” to the tiling-problem instance recalled here has its positive counterpart in Gomory’s theorem, telling us that regardless of where one white and one black square are deleted from an ordinary chessboard, the remaining board can always be tiled by 31 dominoes.
- 5.
The proof-checker Referee is also known by its fancier name ÆtnaNova.
- 6.
In essence, the decision algorithm mentioned here is a solver for Problem 3.4, discussed earlier.
- 7.
As a visible countersign, the formal output parameters of a Theory must carry the Greek letter Θ as a subscript.
References
Ackermann, W.: Die Widerspruchfreiheit der allgemeinen Mengenlehre. Mathematische Annalen 114, 305–315 (1937)
Aczel, P.: Non-Well-Founded Sets. CSLI Lecture Notes, vol. 14. Center for the Study of Language and Information, cop, Stanford (1988)
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1976)
Andersson, S.A., Madigan, D., Perlman, M.D.: A characterization of Markov equivalence classes for acyclic digraphs. Ann. Stat. 25, 502–541 (1997)
Audrito, G., Tomescu, A.I., Wagner, S.G.: Enumeration of the adjunctive hierarchy of hereditarily finite sets. J. Log. Comput. 25 (3), 943–963 (2015)
Bandelt, H.J., Mulder, H.M.: Distance-hereditary graphs. J. Comb. Theory Ser. B 41 (2), 182–208 (1986)
Bang-Jensen, J., Gutin, G.: Digraphs: Theory, Algorithms and Applications. Springer Monographs in Mathematics, 2nd edn. Springer, London (2008)
Barwise, J., Moss, L.: Hypersets. Math. Intell. 13 (4), 31–41 (1991)
Barwise, J., Moss, L.S.: Vicious Circles. CSLI Lecture Notes, Stanford (1996)
Behzad, M., Chartrand, G., Lesniak-Foster, L.: Graphs & Digraphs. Prindle, Weber & Schmidt (1979)
Belinfante, J.G.F.: On computer-assisted proofs in ordinal number theory. J. Autom. Reason. 22 (2), 341–378 (1999)
Bellè, D., Parlamento, F.: Truth in V for ∃ ∗ ∀ ∀-sentences is decidable. J. Symb. Log. 71 (4), 1200–1222 (2006)
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., Klembt, T., Lozin, V.V., Mosca, R.: On independent vertex sets in subclasses of apple-free graphs. Algorithmica 56, 383–393 (2010)
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)
Brandstädt, A., Lozin, V.V., Mosca, R.: Independent sets of maximum weight in apple-free graphs. SIAM J. Discret. Math. 24, 239–254 (2010)
Burstall, R., Goguen, J.: Putting theories together to make specifications. In: Reddy, R. (ed.) Proceedings of 5th International Joint Conference on Artificial Intelligence, Cambridge, MA, pp. 1045–1058 (1977)
Calligaris, P., Omodeo, E.G., Tomescu, A.I.: A proof-checking experiment on representing graphs as membership digraphs. In: Cantone, D., Asmundo, M.N. (eds.) CILC 2013, 28th Italian Conference on Computational Logic, CEUR Workshop Proceedings, Catania, pp. 227–233 (2013)
Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets. Texts and Monographs in Computer Science. Springer, New York (2001)
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)
Casagrande, A., Omodeo, E.G.: Reasoning about connectivity without paths. In: Bistarelli, S., Formisano, A. (eds.) ICTCS’13, Fifteenth Italian Conference on Theoretical Computer Science, CEUR Workshop Proceedings, pp. 93–108 (2014)
Casagrande, A., Piazza, C., Policriti, A.: Is hyper-extensionality preservable under deletions of graph elements? Electron. Notes Theor. Comput. Sci. 322, 103–118 (2016)
Chudnovsky, M., Robertson, N., Seymour, P., Thomas, R.: The strong perfect graph theorem. Ann. Math. 164 (1), 51–229 (2006)
Cohen, P.J.: Set Theory and the Continuum Hypothesis. Mathematics Lecture Note Series. W. A. Benjamin, Inc., Reading, MA(1966)
D’Agostino, G., Omodeo, E.G., Policriti, A., Tomescu, A.I.: Mapping sets and hypersets into numbers. Fundam. Inform. 140 (3–4), 307–328 (2015)
Davis, M.: Applied Nonstandard Analysis. John Wiley & Sons, New York (1977)
Davis, M., Schonberg, E. (eds.): From Linear Operators to Computational Biology: Essays in Memory of Jacob T. Schwartz. Springer (2012)
Dewar, R.: SETL and the Evolution of Programming. In: [27, pp. 39–46] (2012)
Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: {log}: A language for programming in logic with finite sets. J. Log. Program. 28 (1), 1–44 (1996)
Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci. 311 (1–3), 221–256 (2004)
Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22 (5), 861–931 (2000)
Dyer, M., Frieze, A., Jerrum, M.: Approximately counting Hamilton paths and cycles in dense graphs. SIAM J. Comput. 27 (5), 1262–1272 (1998)
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Hartcourt/Academic Press, Burlington (2001)
Erdős, P., Moser, L.: On the representation of directed graphs as unions of orderings. Publ. Math. Inst. Hung. Acad. Sci. Ser. A 9, 125–132 (1964)
Euler, L.: Solutio problematis ad geometriam situs pertinentis. Commentarii academiae scientiarum Petropolitanae 8, 128–140 (1741)
Felgner, U.: Comparison of the axioms of local and universal choice. Fundamenta mathematicae 71 (1), 43–62 (1971)
Ferro, A., Omodeo, E., Schwartz, J.: Decision procedures for some fragments of set theory. In: Bibel, W., Kowalski, R. (eds.) Proceedings of the 5th Conference on Automated Deduction. LNCS, vol. 87, pp. 88–96. Springer, Berlin/New York (1980)
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 Applied Math. 33 (5), 599–608 (1980)
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, Berlin/Heidelberg (2010)
Forti, M., Honsell, F.: Set theory with free construction principles. Annali Scuola Normale Superiore di Pisa, Classe di Scienze IV (10), 493–522 (1983)
Fraenkel, A.A.: The notion of “definite” and the independence of the axiom of choice. In: [46, pp. 284–289]. (The original publication, in German language, is of 1922)
Garey, M.R., Johnson, D.S.: Computers and Intractability; A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1990)
Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: Coarsest partition problems. J. Autom. Reason. 31 (1), 73–103 (2003)
Gödel, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis. Proc. Natl. Acad. Sci. U.S.A. 24 (12), 556–557 (1938)
Harary, F., Palmer, E.: Graphical Enumeration. Academic Press, New York (1973)
van Heijenoort, J. (ed.): From Frege to Gödel – A Source Book in Mathematical Logic, 1879–1931, 3rd printing edn. Source books in the history of the sciences. Harvard University Press (1977)
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)
Hopcroft, J.E.: An nlogn algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of Machines and Computations, pp. 189–196. Academic Press, New York (1971)
Howorka, E.: On metric properties of certain clique graphs. J. Comb. Theory Ser. B 27 (1), 67–74 (1979)
Jech, T.: Set Theory. Springer Monographs in Mathematics, 3rd Millennium edn. Springer, Berlin/Heidelberg (2003)
Keller, J.P., Paige, R.: Program derivation with verified transformations – a case study. Commun. Pure Appl. Math. 48 (9–10), 1053–1113 (1995). Special issue in honor of J.T. Schwartz
Kirby, L.: A hierarchy of hereditarily finite sets. Arch. Math. Log. 47 (2), 143–157 (2008)
König, D.: Theorie der endlichen und unendlichen graphen. Akademische Verlagsgesellschaft Leipzig (1936)
Kunen, K.: Set Theory. Studies in Logic. College Publications (2011)
Levin, D.A., Peresand, Y., Wilmer, E.: Markov Chains and Mixing Times. AMS, Providence (2009)
Lin, R., Olariu, S., Pruesse, G.: An optimal path cover algorithm for cographs. Comput. Math. Appl. 30 (8), 75–83 (1995)
Lisitsa, A., Sazonov, V.: Linear ordering on graphs, anti-founded sets and polynomial time computability. Theor. Comput. Sci. 224, 173–213 (1999)
Lovász, L., Plummer, M.D.: Matching Theory. North-Holland Mathematics Studies. North-Holland/Amsterdam, New York (1986). Includes indexes
Lozin, V.V., Milanič, M., Purcell, C.: Graphs without large apples and the maximum weight independent set problem. Graphs Comb. 30 (2), 395–410 (2014)
Matthews, M.M., Sumner, D.P.: Hamiltonian Results in K 1, 3-Free Graphs. J. Graph Theory 8, 139–146 (1984)
Melançon, G., Philippe, F.: Generating connected acyclic digraphs uniformly at random. Inf. Process. Lett. 90 (4), 209–213 (2004)
Melançon, G., Dutour, I., Bousquet-Mélou, M.: Random generation of directed acyclic graphs. In: Nesetril, J., Noy, M., Serra, O. (eds.) Euroconference on Combinatorics, Graph Theory and Applications (Comb01). Electronic Notes in Discrete Mathematics, vol. 10, pp. 202–207 (2001)
Milanič, M., Rizzi, R., Tomescu, A.I.: Set graphs. II. Complexity of set graph recognition and similar problems. Theor. Comput. Sci. 547, 70–81 (2014)
Milanič, M., Tomescu, A.I.: Set graphs. I. Hereditarily finite sets and extensional acyclic orientations. Discret. Appl. Math. 161 (4–5), 677–690 (2013)
Milanič, M., Tomescu, A.I.: Set graphs. IV. Further connections with claw-freeness. Discret. Appl. Math. 174, 113–121 (2014)
Minty, G.J.: On maximal independent sets of vertices in claw-free graphs. J. Comb. Theory Ser. B 28 (3), 284–304 (1980)
Mostowski, A.: An undecidable arithmetical statement. Fund. Math. 36, 143–164 (1949)
von Neumann, J.: Zur Einführung der trasfiniten Zahlen. Acta Sci. Math. (Szeged) 1 (4–4), 199–208 (1922–23). Available in English translation in [46, pp. 346–354]
von Neumann, J.: Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre. J. für die reine und angewandte Mathematik (160), 227–241, reprinted in [70, pp. 494–508] (1929)
von Neumann, J.: Collected Works, vol. I: Logic, Theory of Sets and Quantum Mechanics. Pergamon Press, New York (1961)
Olariu, S.: The strong perfect graph conjecture for pan-free graphs. J. Comb. Theory Ser. B 47, 187–191 (1989)
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., Parlamento, F., Policriti, A.: Decidability of ∃ ∗ ∀-sentences in membership theories. Math. Log. Q. 42 (1), 41–58 (1996)
Omodeo, E.G., Policriti, A.: The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability. J. Symb. Logic 75 (2), 459–480 (2010)
Omodeo, E.G., Policriti, A.: The Bernays-Schönfinkel-Ramsey class for set theory: decidability. J. Symb. Logic 77 (3), 896–918 (2012)
Omodeo, E.G., Policriti, A., Tomescu, A.I.: Statements of ill-founded infinity in set theory. In: Cégielski, P. (ed.) Studies in Weak Arithmetics. Lecture Notes, vol. 196, pp. 173–199. Center for the Study of Language and Information, Stanford University (2009)
Omodeo, E.G., Policriti, A., Tomescu, A.I.: Infinity, in short. J. Logic Comput. 22 (6), 1391–1403 (2012)
Omodeo, E.G., Policriti, A., Tomescu, A.I.: Set-syllogistics meet combinatorics. Math. Struct. Comput. Sci. 27 (2), 296–310 (2017)
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.: Set graphs. III. Proof Pearl: claw-free graphs mirrored into transitive hereditarily finite sets. J. Automat. Reason. 52 (1), 1–29 (2014)
Omodeo, E.G., Tomescu, A.I.: Set graphs. V. On representing graphs as membership digraphs. J. Log. Comput. 25 (3), 899–919 (2015)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16 (6), 973–989 (1987)
Paige, R., Tarjan, R.E., Bonic, R.: A linear time solution to the single function coarsest partition problem. Theoret. Comput. Sci. 40, 67–84 (1985)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
Parlamento, F., Policriti, A.: Decision procedures for elementary sublanguages of set theory. IX. Unsolvability of the decision problem for a restricted subclass of the Δ 0-formulas in set theory. Commun. Pure Appl. Math. XLI, 221–251 (1988)
Parlamento, F., Policriti, A.: The logically simplest form of the infinity axiom. Proc. Am. Math. Soc. 103 (1), 274–276 (1988)
Parlamento, F., Policriti, A.: Note on “The logically simplest form of the infinity axiom”. Proc. Am. Math. Soc. 108 (1), 285–286 (1990)
Parlamento, F., Policriti, A.: Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability. J. Automat. Reason. 7 (2), 271–284 (1991)
Parlamento, F., Policriti, A.: Expressing infinity without foundation. J. Symb. Logic 56 (4), 1230–1235 (1991)
Parlamento, F., Policriti, A.: Undecidability results for restricted universally quantified formulae of set theory. Commun. Pure Appl. Math. XLVI (1), 57–73 (1993)
Paulson, L.C.: A simple formalization and proof for the mutilated chess board. Logic J. IGPL 9 (3), 499–509 (2001)
Peddicord, R.: The number of full sets with n elements. Proc. Am. Math. Soc. 13, 825–828 (1962)
Piazza, C., Policriti, A.: Ackermann encoding, bisimulations, and OBDDs. Theory Pract. Logic Programm. 4 (5–6), 695–718 (2004)
Policriti, A., Tomescu, A.I.: Counting extensional acyclic digraphs. Inf. Process. Lett. 111 (3), 787–791 (2011)
Policriti, A., Tomescu, A.I.: Markov chain algorithms for generating sets uniformly at random. Ars Math. Contemp. 6 (57–68) (2013)
Prüfer, H.: Neuer Beweis eines Satzes über Permutationen. Arch. Math. Phys. 27, 742–744 (1918)
Quaife, A.: Automated deduction in von Neumann-Bernays-Gödel set theory. J. Autom. Reason. 8 (1), 91–147 (1992)
Ramsey, F.P.: On a problem of formal logic. Proc. Lond. Math. Soc. 30, 264–286 (1930). Read on 13 Dec 1928
Rizzi, R., Tomescu, A.I.: Ranking, unranking and random generation of extensional acyclic digraphs. Inf. Process. Lett. 113 (5–6), 183–187 (2013)
Robinson, R.M.: The theory of classes, a modification of von Neumann’s system. J. Symb. Logic 2, 29–36 (1937)
Robinson, R.W.: Enumeration of acyclic digraphs. In: Proceedings of Second Chapel Hill Conference on Combinatorial Mathematics and its Applications. University of North Carolina, Chapel Hill (1970)
Robinson, R.W.: Counting labeled acyclic digraphs. In: Harary, F. (ed.) New Directions in the Theory of Graphs, pp. 239–273. Academic Press, New York (1973)
Sbihi, N.: Algorithme de recherche d’un stable de cardinalite maximum dans un graphe sans etoile. Discret. Math. 29 (1), 53–76 (1980)
Schwartz, J., Dewar, R., Dubinsky, E., Schonberg, E.: Programming with Sets: An Introduction to SETL. Texts and Monographs in Computer Science. Springer, New York (1986)
Schwartz, J.T., Cantone, D., Omodeo, E.G.: Computational Logic and Set Theory. Springer (2011). Foreword by Martin Davis
Steinsky, B.: Efficient coding of labeled directed acyclic graphs. Soft Comput. 7, 350–356 (2003)
Steinsky, B.: Enumeration of labelled chain graphs and labelled essential directed acyclic graphs. Discret. Math. 270 (1–3), 266–277 (2003)
Sumner, D.: Graphs with 1-factors. Proc. Am. Math. Soc. 42, 8–12 (1974)
Tarski, A.: Sur les ensembles fini. Fundamenta Mathematicae VI, 45–95 (1924)
Tomescu, A.I.: A simpler proof for vertex-pancyclicity of squares of connected claw-free graphs. Discret. Math. 312 (15), 2388–2391 (2012)
Vergnas, M.L.: A note on matchings in graphs. Cahiers Centre Etudes Rech. Opér. 17, 257–260 (1975)
Wagner, S.: Asymptotic enumeration of extensional acyclic digraphs. In: Proceedings of the ANALCO12 Meeting on Analytic Algorithmics and Combinatorics, pp. 1–8 (2012)
West, D.B.: Introduction to Graph Theory. Prentice-Hall, New Jersey (2001)
Zermelo, E.: Untersuchungen über die Grundlagen der Mengenlehre I. In: [46, pp. 199–215] (1908)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Omodeo, E.G., Policriti, A., Tomescu, A.I. (2017). Graphs as Transitive Sets. In: On Sets and Graphs. Springer, Cham. https://doi.org/10.1007/978-3-319-54981-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-54981-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-54980-4
Online ISBN: 978-3-319-54981-1
eBook Packages: Computer ScienceComputer Science (R0)