{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:36Z","timestamp":1759638936982},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_4","type":"book-chapter","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T22:11:57Z","timestamp":1474409517000},"page":"51-68","source":"Crossref","is-referenced-by-count":6,"title":["Relation-Algebraic Verification of Prim\u2019s Minimum Spanning Tree Algorithm"],"prefix":"10.1007","author":[{"given":"Walter","family":"Guttmann","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/3-540-44880-2_27","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"J-R Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D., M\u00e9ry, D.: Formal derivation of spanning trees algorithms. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 457\u2013476. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44880-2_27"},{"key":"4_CR2","unstructured":"Armstrong, A., Foster, S., Struth, G., Weber, T.: Relation algebra. Archive of Formal Proofs (2016). First version (2014)"},{"key":"4_CR3","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2016). First version (2013)"},{"issue":"3","key":"4_CR4","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1016\/j.jlamp.2014.08.003","volume":"84","author":"R Berghammer","year":"2015","unstructured":"Berghammer, R., Fischer, S.: Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures. J. Log. Algebr. Methods Program. 84(3), 341\u2013358 (2015)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Berghammer, R., von Karger, B.: Relational semantics of functional programs. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science, chap. 8, pp. 115\u2013130. Springer, Wien (1997)","DOI":"10.1007\/978-3-7091-6510-2_8"},{"key":"4_CR6","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). doi: 10.1007\/BFb0054283"},{"issue":"3","key":"4_CR7","doi-asserted-by":"crossref","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":"4_CR8","volume-title":"Algebra of Programming","author":"R Bird","year":"1997","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall, Englewood Cliffs (1997)"},{"key":"4_CR9","series-title":"Colloquium Publications","volume-title":"Lattice Theory","author":"G Birkhoff","year":"1967","unstructured":"Birkhoff, G.: Lattice Theory. Colloquium Publications, vol. XXV, 3rd edn. American Mathematical Society, Providence (1967)","edition":"3"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-03429-9_5","volume-title":"Recent Trends in Algebraic Development Techniques","author":"S Bistarelli","year":"2009","unstructured":"Bistarelli, S., Santini, F.: C-semiring frameworks for minimum spanning tree problems. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 56\u201370. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03429-9_5"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116\u2013130. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_11"},{"key":"4_CR12","volume-title":"Lattices and Ordered Algebraic Structures","author":"TS Blyth","year":"2005","unstructured":"Blyth, T.S.: Lattices and Ordered Algebraic Structures. Springer, Berlin (2005)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Comer, S.D.: On connections between information systems, rough sets and algebraic logic. In: Rauszer, C. (ed.) Algebraic Methods in Logic and in Computer Science. Banach Center Publications, vol. 28, pp. 117\u2013124. Institute of Mathematics, Polish Academy of Sciences (1993)","DOI":"10.4064\/-28-1-117-124"},{"key":"4_CR14","volume-title":"Regular Algebra and Finite Machines","author":"JH Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)"},{"key":"4_CR15","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"issue":"2","key":"4_CR16","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1016\/j.jlap.2014.02.005","volume":"83","author":"J Desharnais","year":"2014","unstructured":"Desharnais, J., Grinenko, A., M\u00f6ller, B.: Relational style laws and constructs of linear algebra. J. Log. Algebr. Methods Program. 83(2), 154\u2013168 (2014)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"1","key":"4_CR17","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numerische Mathematik 1(1), 269\u2013271 (1959)","journal-title":"Numerische Mathematik"},{"key":"4_CR18","unstructured":"Freyd, P.J., \u0160\u010dedrov, A.: Categories, Allegories. North-Holland Mathematical Library, vol. 39. Elsevier Science Publishers (1990)"},{"issue":"1","key":"4_CR19","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0022-247X(67)90189-8","volume":"18","author":"JA Goguen","year":"1967","unstructured":"Goguen, J.A.: L-fuzzy sets. J. Math. Anal. Appl. 18(1), 145\u2013174 (1967)","journal-title":"J. Math. Anal. Appl."},{"key":"4_CR20","volume-title":"Graphs, Dioids and Semirings","author":"M Gondran","year":"2008","unstructured":"Gondran, M., Minoux, M.: Graphs, Dioids and Semirings. Springer, Heidelberg (2008)"},{"issue":"1","key":"4_CR21","doi-asserted-by":"crossref","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":"4_CR22","volume-title":"Lattice Theory: First Concepts and Distributive Lattices","author":"G Gr\u00e4tzer","year":"1971","unstructured":"Gr\u00e4tzer, G.: Lattice Theory: First Concepts and Distributive Lattices. W. H. Freeman and Co., San Francisco (1971)"},{"issue":"Part B","key":"4_CR23","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1016\/j.scico.2013.08.008","volume":"85","author":"W Guttmann","year":"2014","unstructured":"Guttmann, W.: Algebras for correctness of sequential computations. Sci. Comput. Program. 85(Part B), 224\u2013240 (2014)","journal-title":"Sci. Comput. Program."},{"key":"4_CR24","unstructured":"Guttmann, W., Struth, G., Weber, T.: A repository for Tarski-Kleene algebras. In: H\u00f6fner, P., McIver, A., Struth, G. (eds.) Automated Theory Engineering. CEUR Workshop Proceedings, vol. 760, pp. 30\u201339 (2011)"},{"issue":"1","key":"4_CR25","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s001650050035","volume":"11","author":"WH Hesselink","year":"1999","unstructured":"Hesselink, W.H.: The verified incremental design of a distributed spanning tree algorithm: extended abstract. Formal Aspects Comput. 11(1), 45\u201355 (1999)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"4_CR26","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1007\/s00165-012-0245-4","volume":"24","author":"P H\u00f6fner","year":"2012","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: Dijkstra, Floyd and Warshall meet Kleene. Formal Aspects Comput. 24(4), 459\u2013476 (2012)","journal-title":"Formal Aspects Comput."},{"key":"4_CR27","unstructured":"Jarn\u00edk, V.: O jist\u00e9m probl\u00e9mu minim\u00e1ln\u00edm (Z dopisu panu O. Bor\u016fvkovi). Pr\u00e1ce moravsk\u00e9 p\u0159\u00edrodov\u011bdeck\u00e9 spole\u010dnosti 6(4), 57\u201363 (1930)"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/11828563_17","volume-title":"Relations and Kleene Algebra in Computer Science","author":"Y Kawahara","year":"2006","unstructured":"Kawahara, Y.: On the cardinality of relations. In: Schmidt, R.A. (ed.) RelMiCS\/AKA 2006. LNCS, vol. 4136, pp. 251\u2013265. Springer, Heidelberg (2006). doi: 10.1007\/11828563_17"},{"issue":"1\u20132","key":"4_CR29","first-page":"1","volume":"33","author":"Y Kawahara","year":"2001","unstructured":"Kawahara, Y., Furusawa, H.: Crispness in Dedekind categories. Bull. Inf. Cybern. 33(1\u20132), 1\u201318 (2001)","journal-title":"Bull. Inf. Cybern."},{"issue":"3\u20134","key":"4_CR30","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0020-0255(99)00017-1","volume":"119","author":"Y Kawahara","year":"1999","unstructured":"Kawahara, Y., Furusawa, H., Mori, M.: Categorical representation theorems of fuzzy relations. Inf. Sci. 119(3\u20134), 235\u2013251 (1999)","journal-title":"Inf. Sci."},{"key":"4_CR31","series-title":"Fundamental Algorithms","volume-title":"The Art of Computer Programming","author":"DE Knuth","year":"1997","unstructured":"Knuth, D.E.: The Art of Computer Programming. Fundamental Algorithms, vol. 1, 3rd edn. Addison-Wesley, Reading (1997)","edition":"3"},{"issue":"2","key":"4_CR32","doi-asserted-by":"crossref","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":"2","key":"4_CR33","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s00165-014-0316-9","volume":"27","author":"HD Macedo","year":"2015","unstructured":"Macedo, H.D., Oliveira, J.N.: A linear algebra approach to OLAP. Formal Aspects Comput. 27(2), 283\u2013307 (2015)","journal-title":"Formal Aspects Comput."},{"issue":"1\u20132","key":"4_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(95)00082-8","volume":"160","author":"RD Maddux","year":"1996","unstructured":"Maddux, R.D.: Relation-algebraic semantics. Theor. Comput. Sci. 160(1\u20132), 1\u201385 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR35","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/j.cosrev.2008.10.002","volume":"2","author":"M Mare\u0161","year":"2008","unstructured":"Mare\u0161, M.: The saga of minimum spanning trees. Comput. Sci. Rev. 2(3), 165\u2013221 (2008)","journal-title":"Comput. Sci. Rev."},{"issue":"2","key":"4_CR36","doi-asserted-by":"crossref","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":"4_CR37","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":"4_CR38","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03153-3_5","volume-title":"Language Engineering and Rigorous Software Development","author":"JN Oliveira","year":"2009","unstructured":"Oliveira, J.N.: Extended static checking by calculation using the pointfree transform. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol. 5520, pp. 195\u2013251. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03153-3_5"},{"issue":"4","key":"4_CR40","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/s00165-012-0240-9","volume":"24","author":"JN Oliveira","year":"2012","unstructured":"Oliveira, J.N.: Towards a linear algebra of programming. Formal Aspects Comput. 24(4), 433\u2013458 (2012)","journal-title":"Formal Aspects Comput."},{"issue":"6","key":"4_CR41","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1142\/S0129054113400145","volume":"24","author":"JN Oliveira","year":"2013","unstructured":"Oliveira, J.N.: Weighted automata as coalgebras in categories of matrices. Int. J. Found. Comput. Sci. 24(6), 709\u2013728 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"4_CR42","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":"6","key":"4_CR43","doi-asserted-by":"crossref","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":"4_CR44","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-77968-8","volume-title":"Relations and Graphs","author":"G Schmidt","year":"1993","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and Graphs. Springer, Berlin (1993)"},{"issue":"2","key":"4_CR45","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.jlap.2005.04.001","volume":"66","author":"G Struth","year":"2006","unstructured":"Struth, G.: Abstract abstract reduction. J. Log. Algebr. Program. 66(2), 239\u2013270 (2006)","journal-title":"J. Log. Algebr. Program."},{"issue":"3","key":"4_CR46","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. J. Symbol. Log. 6(3), 73\u201389 (1941)","journal-title":"J. Symbol. Log."},{"issue":"3\u20134","key":"4_CR47","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/S0020-0255(01)00167-0","volume":"139","author":"M Winter","year":"2001","unstructured":"Winter, M.: A new algebraic approach to L-fuzzy relations convenient to study crispness. Inf. Sci. 139(3\u20134), 233\u2013252 (2001)","journal-title":"Inf. Sci."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T16:29:36Z","timestamp":1568392176000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}