{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T16:07:57Z","timestamp":1757779677986,"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_14","type":"book-chapter","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T23:06:25Z","timestamp":1634857585000},"page":"225-240","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Relation-Algebraic Verification of\u00a0Bor\u016fvka\u2019s Minimum Spanning Tree\u00a0Algorithm"],"prefix":"10.1007","author":[{"given":"Walter","family":"Guttmann","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Robinson-O\u2019Brien","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"key":"14_CR1","unstructured":"Balbes, R., Dwinger, P.: Distributive Lattices. University of Missouri Press (1974)"},{"key":"14_CR2","unstructured":"Berge, C., Ghouila-Houri, A.: Programming, Games and Transportation Networks. Wiley, Methuen (1965)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BFb0054283","volume-title":"Mathematics of Program Construction","author":"R Berghammer","year":"1998","unstructured":"Berghammer, R., von Karger, B., Wolf, A.: Relation-algebraic derivation of spanning tree algorithms. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 23\u201343. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054283"},{"issue":"3","key":"14_CR4","doi-asserted-by":"publisher","first-page":"636","DOI":"10.1016\/j.ejor.2012.11.025","volume":"226","author":"R Berghammer","year":"2013","unstructured":"Berghammer, R., Rusinowska, A., de Swart, H.: Computing tournament solutions using relation algebra and RelView. Eur. J. Oper. Res. 226(3), 636\u2013645 (2013)","journal-title":"Eur. J. Oper. Res."},{"key":"14_CR5","unstructured":"Birkhoff, G.: Lattice Theory, Colloquium Publications, vol. XXV, 3rd edn., American Mathematical Society (1967)"},{"issue":"3","key":"14_CR6","first-page":"37","volume":"3","author":"O Bor\u016fvka","year":"1926","unstructured":"Bor\u016fvka, O.: O jist\u00e9m probl\u00e9mu minim\u00e1ln\u00edm. Pr\u00e1ce moravsk\u00e9 p\u0159\u00edrodov\u011bdeck\u00e9 spole\u010dnosti 3(3), 37\u201358 (1926)","journal-title":"Pr\u00e1ce moravsk\u00e9 p\u0159\u00edrodov\u011bdeck\u00e9 spole\u010dnosti"},{"issue":"6","key":"14_CR7","doi-asserted-by":"publisher","first-page":"1028","DOI":"10.1145\/355541.355562","volume":"47","author":"B Chazelle","year":"2000","unstructured":"Chazelle, B.: A minimum spanning tree algorithm with inverse-Ackermann type complexity. J. ACM 47(6), 1028\u20131047 (2000)","journal-title":"J. ACM"},{"key":"14_CR8","first-page":"310","volume":"206","author":"G Choquet","year":"1938","unstructured":"Choquet, G.: \u00c9tude de certains r\u00e9seaux de routes. C. R. Hebd. Seances Acad. Sci. 206, 310\u2013313 (1938)","journal-title":"C. R. Hebd. Seances Acad. Sci."},{"key":"14_CR9","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971)"},{"issue":"3\u20134","key":"14_CR10","doi-asserted-by":"publisher","first-page":"282","DOI":"10.4064\/cm-2-3-4-282-285","volume":"2","author":"K Florek","year":"1951","unstructured":"Florek, K., \u0141ukaszewicz, J., Perkal, J., Steinhaus, H., Zubrzycki, S.: Sur la liaison et la division des points d\u2019un ensemble fini. Colloq. Math. 2(3\u20134), 282\u2013285 (1951)","journal-title":"Colloq. Math."},{"key":"14_CR11","unstructured":"Frias, M.F., Aguayo, N., Novak, B.: Development of graph algorithms with fork algebras. In: XIX Conferencia Latinoamericana de Inform\u00e1tica, pp. 529\u2013554 (1993)"},{"issue":"1","key":"14_CR12","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/MAHC.1985.10011","volume":"7","author":"RL Graham","year":"1985","unstructured":"Graham, R.L., Hell, P.: On the history of the minimum spanning tree problem. Ann. Hist. Comput. 7(1), 43\u201357 (1985)","journal-title":"Ann. Hist. Comput."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-46750-4_4","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"W Guttmann","year":"2016","unstructured":"Guttmann, W.: Relation-algebraic verification of Prim\u2019s minimum spanning tree algorithm. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 51\u201368. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_4"},{"key":"14_CR14","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. Theoret. Comput. Sci. 744, 37\u201355 (2018)","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR15","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 Methods Program. 101, 132\u2013150 (2018)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"14_CR16","unstructured":"Guttmann, W., Robinson-O\u2019Brien, N.: Relational minimum spanning tree algorithms. Archive of Formal Proofs (2020). Formal proof development. https:\/\/isa-afp.org\/entries\/Relational_Minimum_Spanning_Trees.html"},{"key":"14_CR17","unstructured":"Haslbeck, M.P.L., Lammich, P., Biendarra, J.: Kruskal\u2019s algorithm for minimum spanning forest. Archive of Formal Proofs (2019). Formal proof development. https:\/\/isa-afp.org\/entries\/Kruskal.html"},{"issue":"2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/201019.201022","volume":"42","author":"DR Karger","year":"1995","unstructured":"Karger, D.R., Klein, P.N., Tarjan, R.E.: A randomized linear-time algorithm to find minimum spanning trees. J. ACM 42(2), 321\u2013328 (1995)","journal-title":"J. ACM"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11730095_13","volume-title":"Evolutionary Computation in Combinatorial Optimization","author":"B Kehden","year":"2006","unstructured":"Kehden, B., Neumann, F.: A relation-algebraic view on evolutionary algorithms for some graph problems. In: Gottlieb, J., Raidl, G.R. (eds.) EvoCOP 2006. LNCS, vol. 3906, pp. 147\u2013158. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730095_13"},{"issue":"2","key":"14_CR20","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":"14_CR21","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."},{"key":"14_CR22","unstructured":"Lammich, P., Nipkow, T.: Proof pearl: purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). LIPIcs: Leibniz International Proceedings in Informatics, vol. 141, pp. 23:1\u201323:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"14_CR23","unstructured":"Maddux, R.D.: Relation Algebras. Elsevier B.V. (2006)"},{"issue":"1\u20133","key":"14_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0012-365X(00)00224-7","volume":"233","author":"J Ne\u0161et\u0159il","year":"2001","unstructured":"Ne\u0161et\u0159il, J., Milkov\u00e1, E., Ne\u0161et\u0159ilov\u00e1, H.: Otakar Bor\u016fvka on minimum spanning tree problem \u2013 translation of both the 1926 papers, comments, history. Discret. Math. 233(1\u20133), 3\u201336 (2001)","journal-title":"Discret. Math."},{"issue":"2","key":"14_CR25","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":"14_CR26","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":"14_CR27","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":"14_CR28","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms. A biased survey. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis, ATVA 2020. LNCS, vol. 12302, pp. 25\u201353. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_2","DOI":"10.1007\/978-3-030-59152-6_2"},{"issue":"6","key":"14_CR29","doi-asserted-by":"publisher","first-page":"1389","DOI":"10.1002\/j.1538-7305.1957.tb01515.x","volume":"36","author":"RC Prim","year":"1957","unstructured":"Prim, R.C.: Shortest connection networks and some generalizations. Bell Syst. Tech. J. 36(6), 1389\u20131401 (1957)","journal-title":"Bell Syst. Tech. J."},{"key":"14_CR30","unstructured":"Robinson-O\u2019Brien, N.: A formal correctness proof of Bor\u016fvka\u2019s minimum spanning tree algorithm. Master\u2019s thesis, University of Canterbury (2020). https:\/\/doi.org\/10.26021\/10196"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and Graphs. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-3-642-77968-8","DOI":"10.1007\/978-3-642-77968-8"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Tarjan, R.E.: Data Structures and Network Algorithms, CBMS-NSF Regional Conference Series in Applied Mathematics, vol. 44. SIAM (1983)","DOI":"10.1137\/1.9781611970265"},{"issue":"3","key":"14_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"},{"issue":"1","key":"14_CR34","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0020-0190(75)90056-3","volume":"4","author":"ACC Yao","year":"1975","unstructured":"Yao, A.C.C.: An $$\\text{ O }(|E| \\log \\log |V|)$$ algorithm for finding minimum spanning trees. Inf. Process. Lett. 4(1), 21\u201323 (1975)","journal-title":"Inf. Process. Lett."}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T00:49:53Z","timestamp":1634863793000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88701-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887001","9783030887018"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88701-8_14","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"}}]}}