{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T13:31:42Z","timestamp":1743082302178,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030887001"},{"type":"electronic","value":"9783030887018"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88701-8_13","type":"book-chapter","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T23:06:25Z","timestamp":1634857585000},"page":"209-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Second-Order Properties of Undirected Graphs"],"prefix":"10.1007","author":[{"given":"Walter","family":"Guttmann","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"issue":"3\u20134","key":"13_CR1","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0020-0255(99)00012-2","volume":"119","author":"R Berghammer","year":"1999","unstructured":"Berghammer, R.: Combining relational calculus and the Dijkstra-Gries method for deriving relational programs. Inf. Sci. 119(3\u20134), 155\u2013171 (1999)","journal-title":"Inf. Sci."},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"100590","DOI":"10.1016\/j.jlamp.2020.100590","volume":"117","author":"R Berghammer","year":"2020","unstructured":"Berghammer, R., Furusawa, H., Guttmann, W., H\u00f6fner, P.: Relational characterisations of paths. J. Log. Algebraic Meth. Program. 117, 100590 (2020)","journal-title":"J. Log. Algebraic Meth. Program."},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-13321-3_4","volume-title":"Mathematics of Program Construction","author":"R Berghammer","year":"2010","unstructured":"Berghammer, R., Struth, G.: On automated program construction and verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 22\u201341. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13321-3_4"},{"key":"13_CR4","unstructured":"Bird, R., Wadler, P.: Introduction to Functional Programming. Prentice Hall (1988)"},{"issue":"1","key":"13_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"13_CR7","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic, vol. 1. North-Holland Publishing Company (1958)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Diestel, R.: Graph Theory, 3rd edn. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-642-14279-6_7"},{"key":"13_CR9","unstructured":"Dwinger, P.: Introduction to Boolean Algebras, 2nd edn. Physica-Verlag (1971)"},{"key":"13_CR10","unstructured":"Freyd, P.J., \u0160\u010dedrov, A.: Categories, Allegories, North-Holland Mathematical Library, vol. 39. Elsevier Science Publishers (1990)"},{"issue":"5","key":"13_CR11","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/0020-0190(88)90089-0","volume":"27","author":"HN Gabow","year":"1988","unstructured":"Gabow, H.N., Tarjan, R.E.: A linear-time algorithm for finding a minimum spanning pseudoforest. Inf. Process. Lett. 27(5), 259\u2013263 (1988)","journal-title":"Inf. Process. Lett."},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Givant, S.: Introduction to Relation Algebras, Relation Algebras, vol. 1. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-65235-1","DOI":"10.1007\/978-3-319-65235-1"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.tcs.2018.04.012","volume":"744","author":"W Guttmann","year":"2018","unstructured":"Guttmann, W.: An algebraic framework for minimum spanning tree problems. Theor. Comput. Sci. 744, 37\u201355 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1016\/j.jlamp.2018.09.005","volume":"101","author":"W Guttmann","year":"2018","unstructured":"Guttmann, W.: Verifying minimum spanning tree algorithms with Stone relation algebras. J. Log. Algebraic Meth. Program. 101, 132\u2013150 (2018)","journal-title":"J. Log. Algebraic Meth. Program."},{"key":"13_CR15","unstructured":"Guttmann, W.: Relational forests. Archive of Formal Proofs (2021). https:\/\/www.isa-afp.org\/entries\/Relational_Forests.html"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01191538","volume":"32","author":"P Jipsen","year":"1994","unstructured":"Jipsen, P., Luk\u00e1cs, E.: Minimal relation algebras. Algebra Univers. 32(2), 189\u2013203 (1994)","journal-title":"Algebra Univers."},{"issue":"2","key":"13_CR17","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994)","journal-title":"Inf. Comput."},{"issue":"1","key":"13_CR18","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1090\/S0002-9939-1956-0078686-7","volume":"7","author":"JB Kruskal Jr","year":"1956","unstructured":"Kruskal, J.B., Jr.: On the shortest spanning subtree of a graph and the traveling salesman problem. Proc. Am. Math. Soc. 7(1), 48\u201350 (1956)","journal-title":"Proc. Am. Math. Soc."},{"issue":"1","key":"13_CR19","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1090\/S0002-9947-1991-1049616-1","volume":"328","author":"RD Maddux","year":"1991","unstructured":"Maddux, R.D.: Pair-dense relation algebras. Trans. Am. Math. Soc. 328(1), 83\u2013131 (1991)","journal-title":"Trans. Am. Math. Soc."},{"key":"13_CR20","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). https:\/\/www.cs.unm.edu\/~mccune\/prover9\/. Accessed 10 Aug 2021"},{"key":"13_CR21","first-page":"51","volume":"63","author":"B Monjardet","year":"1978","unstructured":"Monjardet, B.: Axiomatiques et propri\u00e9t\u00e9s des quasi-ordres. Math\u00e9matiques et sciences humaines 63, 51\u201382 (1978)","journal-title":"Math\u00e9matiques et sciences humaines"},{"key":"13_CR22","unstructured":"Ng, K.C.: Relation Algebras with Transitive Closure. Ph.D. thesis, University of California, Berkeley (1984)"},{"issue":"2","key":"13_CR23","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: towards a mechanized semantics textbook. Formal Aspects Comput. 10(2), 171\u2013186 (1998)","journal-title":"Formal Aspects Comput."},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer Academic Publishers (2002)","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"13_CR26","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 3\u201313 (2010)"},{"issue":"2","key":"13_CR27","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1002\/net.3230120206","volume":"12","author":"JC Picard","year":"1982","unstructured":"Picard, J.C., Queyranne, M.: A network flow solution to some nonlinear 0\u20131 programming problems, with applications to graph theory. Networks 12(2), 141\u2013159 (1982)","journal-title":"Networks"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Schmidt, G.: Relational Mathematics. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511778810"},{"issue":"1","key":"13_CR29","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0012-365X(85)90064-0","volume":"54","author":"G Schmidt","year":"1985","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relation algebras: concept of points and representability. Discret. Math. 54(1), 83\u201392 (1985)","journal-title":"Discret. Math."},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relationen und Graphen. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/978-3-642-83608-4","DOI":"10.1007\/978-3-642-83608-4"},{"issue":"3\u20134","key":"13_CR31","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BF01448013","volume":"92","author":"M Sch\u00f6nfinkel","year":"1924","unstructured":"Sch\u00f6nfinkel, M.: \u00dcber die Bausteine der mathematischen Logik. Math. Ann. 92(3\u20134), 305\u2013316 (1924)","journal-title":"Math. Ann."},{"key":"13_CR32","doi-asserted-by":"publisher","first-page":"386","DOI":"10.4064\/fm-16-1-386-389","volume":"16","author":"E Szpilrajn","year":"1930","unstructured":"Szpilrajn, E.: Sur l\u2019extension de l\u2019ordre partiel. Fundam. Math. 16, 386\u2013389 (1930)","journal-title":"Fundam. Math."},{"issue":"3","key":"13_CR33","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. J. Symbolic Logic 6(3), 73\u201389 (1941)","journal-title":"J. Symbolic Logic"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_12"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88701-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T05:56:29Z","timestamp":1673589389000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88701-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887001","9783030887018"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88701-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marseille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ramics19.lis-lab.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}