{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T11:44:01Z","timestamp":1710503041758},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,11,30]],"date-time":"2012-11-30T00:00:00Z","timestamp":1354233600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,1]]},"DOI":"10.1007\/s10817-012-9272-3","type":"journal-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T15:52:25Z","timestamp":1354204345000},"page":"1-29","source":"Crossref","is-referenced-by-count":6,"title":["Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets"],"prefix":"10.1007","volume":"52","author":[{"given":"Eugenio G.","family":"Omodeo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandru I.","family":"Tomescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,11,30]]},"reference":[{"issue":"1\u20133","key":"9272_CR1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/S0012-365X(97)00023-X","volume":"179","author":"A Ainouche","year":"1998","unstructured":"Ainouche, A.: Quasi-claw-free graphs. Discrete Math. 179(1\u20133), 13\u201326 (1998)","journal-title":"Discrete Math."},{"key":"9272_CR2","doi-asserted-by":"crossref","unstructured":"Alkassar, E., B\u00f6hme, 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\u201382. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_7"},{"key":"9272_CR3","volume-title":"Digraphs Theory, Algorithms and Applications","author":"J Bang-Jensen","year":"2000","unstructured":"Bang-Jensen, J., Gutin, G.: Digraphs Theory, Algorithms and Applications, 1st edn. Springer, Berlin (2000)","edition":"1"},{"key":"9272_CR4","volume-title":"Beitr\u00e4ge zur Graphentheorie, chap. Derived graphs and digraphs.","author":"L Beineke","year":"1968","unstructured":"Beineke, L.: Beitr\u00e4ge zur Graphentheorie, chap. Derived graphs and digraphs. Teubner, Leipzig (1968)"},{"key":"9272_CR5","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0021-9800(70)80019-9","volume":"9","author":"L Beineke","year":"1970","unstructured":"Beineke, L.: Characterizations of derived graphs. J. Comb. Theory, Ser. B 9, 129\u2013135 (1970)","journal-title":"J. Comb. Theory, Ser. B"},{"key":"9272_CR6","first-page":"10","volume":"34","author":"JGF Belinfante","year":"1996","unstructured":"Belinfante, J.G.F.: On a modification of G\u00f6del\u2019s algorithm for class formation. AAR Newsletter 34, 10\u201315 (1996)","journal-title":"AAR Newsletter"},{"issue":"2","key":"9272_CR7","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1023\/A:1006010913494","volume":"22","author":"JGF Belinfante","year":"1999","unstructured":"Belinfante, J.G.F.: On computer-assisted proofs in ordinal number theory. J. Autom. Reason. 22(2), 341\u2013378 (1999)","journal-title":"J. Autom. Reason."},{"key":"9272_CR8","doi-asserted-by":"crossref","unstructured":"Belinfante, J.G.F.: G\u00f6del\u2019s algorithm for class formation. In: McAllester, D.A. (ed.) CADE, Lecture Notes in Computer Science, vol. 1831, pp. 132\u2013147. Springer (2000)","DOI":"10.1007\/10721959_9"},{"issue":"1\u20132","key":"9272_CR9","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/S0747-7171(03)00023-3","volume":"36","author":"JGF Belinfante","year":"2003","unstructured":"Belinfante, J.G.F.: Computer proofs about finite and regular sets: the unifying concept of subvariance. J. Symb. Comput. 36(1\u20132), 271\u2013285 (2003)","journal-title":"J. Symb. Comput."},{"key":"9272_CR10","doi-asserted-by":"crossref","unstructured":"Belinfante, J.G.F.: Reasoning about iteration in G\u00f6del\u2019s class theory. In: Baader, F. (ed.) CADE, Lecture Notes in Computer Science, vol. 2741, pp. 228\u2013242. Springer (2003)","DOI":"10.1007\/978-3-540-45085-6_18"},{"key":"9272_CR11","first-page":"114","volume":"10","author":"C Berge","year":"1961","unstructured":"Berge, C.: F\u00e4rbung von Graphen, deren s\u00e4mtliche bzw. deren ungerade Kreise starr sind. Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10, 114 (1961)","journal-title":"Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe"},{"issue":"3","key":"9272_CR12","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"RS Boyer","year":"1986","unstructured":"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\u00f6del\u2019s axioms. J. Autom. Reason. 2(3), 287\u2013327 (1986)","journal-title":"J. Autom. Reason."},{"key":"9272_CR13","doi-asserted-by":"crossref","DOI":"10.1137\/1.9780898719796","volume-title":"Graph Classes: A Survey, Monographs on Discrete Mathematics and Applications, vol.\u00a03","author":"A Brandst\u00e4dt","year":"1999","unstructured":"Brandst\u00e4dt, A., Le, V.B., Spinrad, J.P.: Graph Classes: A Survey, Monographs on Discrete Mathematics and Applications, vol.\u00a03. SIAM Society for Industrial and Applied Mathematics, Philadelphia (1999)"},{"key":"9272_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013219. Springer (2006)","DOI":"10.1007\/11814771_19"},{"key":"9272_CR15","unstructured":"Burstall, R., Goguen, J.: Putting theories together to make specifications. In: Reddy, R. (ed.) Proc. 5th International Joint Conference on Artificial Intelligence, pp. 1045\u20131058. Cambridge, MA (1977)"},{"key":"9272_CR16","doi-asserted-by":"crossref","unstructured":"Cantone, D., Omodeo, E.G., Schwartz, J.T., Ursino, P.: Notes from the logbook of a proof-checker\u2019s 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\u2013207. Springer (2003)","DOI":"10.1007\/978-3-540-39910-0_8"},{"issue":"1","key":"9272_CR17","doi-asserted-by":"crossref","first-page":"51","DOI":"10.4007\/annals.2006.164.51","volume":"164","author":"M Chudnovsky","year":"2006","unstructured":"Chudnovsky, M., Robertson, N., Seymour, P., Thomas, R.: The strong perfect graph theorem. Ann. Math. 164(1), 51\u2013229 (2006)","journal-title":"Ann. Math."},{"issue":"6","key":"9272_CR18","doi-asserted-by":"crossref","first-page":"867","DOI":"10.1016\/j.jctb.2007.02.002","volume":"97","author":"M Chudnovsky","year":"2007","unstructured":"Chudnovsky, M., Seymour, P.D.: Claw-free graphs. I. Orientable prismatic graphs. J. Comb. Theory, Ser. B 97(6), 867\u2013903 (2007)","journal-title":"J. Comb. Theory, Ser. B"},{"issue":"6","key":"9272_CR19","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1016\/j.jctb.2010.04.005","volume":"100","author":"M Chudnovsky","year":"2010","unstructured":"Chudnovsky, M., Seymour, P.D.: Claw-free graphs. VI. Colouring. J. Comb. Theory, Ser. B 100(6), 560\u2013572 (2010)","journal-title":"Colouring. J. Comb. Theory, Ser. B"},{"issue":"3","key":"9272_CR20","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1002\/(SICI)1097-0118(199611)23:3<309::AID-JGT11>3.0.CO;2-9","volume":"23","author":"N Eaton","year":"1996","unstructured":"Eaton, N., Grable, D.A.: Set intersection representations for almost all graphs. J. Graph Theory 23(3), 309\u2013320 (1996)","journal-title":"J. Graph Theory"},{"key":"9272_CR21","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0012-365X(96)00045-3","volume":"164","author":"R Faudree","year":"1997","unstructured":"Faudree, R., Flandrin, E., Ryj\u00e1\u010dek, Z.: Claw-flee graphs\u2014a survey. Discrete Math. 164, 87\u2013147 (1997)","journal-title":"Discrete Math."},{"issue":"5","key":"9272_CR22","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"33","author":"A Ferro","year":"1980","unstructured":"Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory.\u00a0I. Multi-level syllogistic and some extensions. Commun. Pure Appl. Math. 33(5), 599\u2013608 (1980)","journal-title":"Commun. Pure Appl. Math."},{"key":"9272_CR23","doi-asserted-by":"crossref","unstructured":"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.\u00a087, pp. 88\u201396. Springer-Verlag (1980)","DOI":"10.1007\/3-540-10009-1_8"},{"key":"9272_CR24","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer Berlin\/Heidelberg (2005)"},{"key":"9272_CR25","doi-asserted-by":"crossref","unstructured":"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\u201363. Springer (2010)","DOI":"10.1007\/978-3-642-14309-0_3"},{"issue":"2","key":"9272_CR26","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0012-365X(85)90039-1","volume":"55","author":"MC Golumbic","year":"1985","unstructured":"Golumbic, M.C.: Interval graphs and related topics. Discrete Math. 55(2), 113\u2013121 (1985)","journal-title":"Discrete Math."},{"issue":"1","key":"9272_CR27","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/BF01864170","volume":"4","author":"MC Golumbic","year":"1988","unstructured":"Golumbic, M.C.: Algorithmic aspects of intersection graphs and representation hypergraphs. Graphs Comb. 4(1), 307\u2013321 (1988)","journal-title":"Graphs Comb."},{"issue":"11","key":"9272_CR28","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. Not. Am. Math. Soc. 55(11), 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"4","key":"9272_CR29","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1002\/jgt.3190090415","volume":"9","author":"G Hendry","year":"1985","unstructured":"Hendry, G., Vogler, W.: The square of a connected S(K 1,3)-free graph is vertex pancyclic. J. Graph Theory 9(4), 535\u2013537 (1985)","journal-title":"J. Graph Theory"},{"issue":"4","key":"9272_CR30","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1002\/jgt.3190090416","volume":"9","author":"M J\u00fcnger","year":"1985","unstructured":"J\u00fcnger, M., Reinelt, G., Pulleyblank, W.R.: On partitioning the edges of graphs into connected subgraphs. J. Graph Theory 9(4), 539\u2013549 (1985)","journal-title":"J. Graph Theory"},{"key":"9272_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-02308-2","volume-title":"Basic Set Theory","author":"A Levy","year":"1979","unstructured":"Levy, A.: Basic Set Theory. Springer, Berlin (1979)"},{"key":"9272_CR32","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1002\/jgt.3190080116","volume":"8","author":"MM Matthews","year":"1984","unstructured":"Matthews, M.M., Sumner, D.P.: Hamiltonian Results in K 1,3-Free Graphs. J. Graph Theory 8, 139\u2013146 (1984)","journal-title":"J. Graph Theory"},{"issue":"1","key":"9272_CR33","first-page":"3","volume":"4","author":"R Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and its Applications 4(1), 3\u201324 (2005)","journal-title":"Mechanized Mathematics and its Applications"},{"key":"9272_CR34","author":"M Milani\u010d","year":"2011","unstructured":"Milani\u010d, 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","journal-title":"Discrete Appl. Math."},{"key":"9272_CR35","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/11541868_24","volume-title":"Proceedings of the 18th international conference on Theorem Proving in Higher Order Logics, TPHOLs\u201905","author":"JS Moore","year":"2005","unstructured":"Moore, J.S., Zhang, Q.: Proof pearl: Dijkstra\u2019s shortest path algorithm verified with ACL2. In: Proceedings of the 18th international conference on Theorem Proving in Higher Order Logics, TPHOLs\u201905, pp. 373\u2013384. Springer-Verlag, Berlin, Heidelberg (2005)"},{"key":"9272_CR36","unstructured":"Nordhoff, B., Lammich, P.: Dijkstra\u2019s shortest path algorithm. Archive of Formal Proofs (2012). http:\/\/afp.sourceforge.net\/entries\/Dijkstra_Shortest_Path.shtml , Formal proof development"},{"key":"9272_CR37","doi-asserted-by":"crossref","unstructured":"Omodeo, E.G.: The Ref proof-checker and its \u201ccommon shared scenario\u201d. In: Davis, M., Schonberg, E. (eds.) From Linear Operators to Computational Biology: Essays in Memory of Jacob T. Schwartz, pp. 121\u2013131. Springer (2012)","DOI":"10.1007\/978-1-4471-4282-9_8"},{"key":"9272_CR38","doi-asserted-by":"crossref","unstructured":"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\u2014Essays Dedicated to Luigia Carlucci Aiello, LNAI, vol. 4155, pp. 117\u2013139. Springer (2006)","DOI":"10.1007\/11829263_7"},{"key":"9272_CR39","doi-asserted-by":"crossref","unstructured":"Omodeo, E.G., Schwartz, J.T.: A \u2018theory\u2019 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\u2013230. Springer (2002)","DOI":"10.1007\/3-540-45632-5_9"},{"key":"9272_CR40","unstructured":"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\u2013167. Springer (2012)"},{"issue":"3","key":"9272_CR41","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1016\/S0095-8956(76)80005-6","volume":"21","author":"KR Parthasarathy","year":"1976","unstructured":"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\u2013223 (1976)","journal-title":"J. Combin. Theory, Ser. B"},{"issue":"1","key":"9272_CR42","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A Quaife","year":"1992","unstructured":"Quaife, A.: Automated deduction in von Neumann-Bernays-G\u00f6del set theory. J. Automat. Reason. 8(1), 91\u2013147 (1992)","journal-title":"J. Automat. Reason."},{"issue":"5","key":"9272_CR43","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1002\/jgt.3190180505","volume":"18","author":"Z Ryj\u00e1\u010dek","year":"1994","unstructured":"Ryj\u00e1\u010dek, Z.: Almost claw-free graphs. J. Graph Theory 18(5), 469\u2013477 (1994)","journal-title":"J. Graph Theory"},{"key":"9272_CR44","doi-asserted-by":"crossref","unstructured":"Schwartz, J.T., Cantone, D., Omodeo, E.G.: Computational Logic and Set Theory. Springer (2011). Foreword by Martin Davis","DOI":"10.1007\/978-0-85729-808-9"},{"key":"9272_CR45","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1090\/S0002-9939-1974-0323648-6","volume":"42","author":"D Sumner","year":"1974","unstructured":"Sumner, D.: Graphs with 1-factors. Proc. Amer. Math. Soc. 42, 8\u201312 (1974)","journal-title":"Proc. Amer. Math. Soc."},{"key":"9272_CR46","doi-asserted-by":"crossref","first-page":"303","DOI":"10.4064\/fm-33-1-303-307","volume":"33","author":"E Szpilrajn-Marczewski","year":"1945","unstructured":"Szpilrajn-Marczewski, E.: Sur deux propri\u00e9t\u00e9s des classes d\u2019ensemble. Fund. Math. 33, 303\u2013307 (1945)","journal-title":"Fund. Math."},{"key":"9272_CR47","doi-asserted-by":"crossref","first-page":"45","DOI":"10.4064\/fm-6-1-45-95","volume":"VI","author":"A Tarski","year":"1924","unstructured":"Tarski, A.: Sur les ensembles fini. Fund. Math. VI, 45\u201395 (1924)","journal-title":"Fund. Math."},{"key":"9272_CR48","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: A formalization of set theory without variables. In: Colloquium Publications, vol. 41. American Mathematical Society (1987)","DOI":"10.1090\/coll\/041"},{"issue":"4","key":"9272_CR49","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/s10817-010-9206-x","volume":"48","author":"F Verbeek","year":"2012","unstructured":"Verbeek, F., Schmaltz, J.: Proof pearl: a formal proof of Dally and Seitz\u2019 necessary and sufficient condition for deadlock-free routing in interconnection networks. J. Autom. Reason. 48(4), 419\u2013439 (2012)","journal-title":"J. Autom. Reason."},{"key":"9272_CR50","first-page":"257","volume":"17","author":"ML Vergnas","year":"1975","unstructured":"Vergnas, M.L.: A note on matchings in graphs. Cahiers Centre Etudes Rech. Op\u00e9r. 17, 257\u2013260 (1975)","journal-title":"Cahiers Centre Etudes Rech. Op\u00e9r."},{"issue":"3\u20134","key":"9272_CR51","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1023\/A:1021935419355","volume":"29","author":"M Wenzel","year":"2002","unstructured":"Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3\u20134), 389\u2013411 (2002)","journal-title":"J. Autom. Reason."},{"key":"9272_CR52","unstructured":"Wiedijk, F.: Mizar: An impression. http:\/\/www.cs.ru.nl\/~freek\/mizar\/mizarintro.ps.gz (1999). Accessed 1 April 2012"},{"issue":"1","key":"9272_CR53","first-page":"93","volume":"5","author":"L Wos","year":"1989","unstructured":"Wos, L.: The problem of finding an inference rule for set theory. J. Autom. Reason. 5(1), 93\u201395 (1989)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9272-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9272-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9272-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T15:59:49Z","timestamp":1643731189000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9272-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,30]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["9272"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9272-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,30]]}}}