{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:30:38Z","timestamp":1777426238246,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540730835","type":"print"},{"value":"9783540730866","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_26","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T10:57:56Z","timestamp":1187089076000},"page":"327-341","source":"Crossref","is-referenced-by-count":7,"title":["Alternative Aggregates in Mizar"],"prefix":"10.1007","author":[{"given":"Gilbert","family":"Lee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Rudnicki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"26_CR1","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F.J.Z.: A constructive algebraic hierarchy in Coq. Journal of Symbolic Computation\u00a034(4), 271\u2013286 (2002), See also http:\/\/www.cs.ru.nl\/~freek\/pubs","journal-title":"Journal of Symbolic Computation"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_7","volume-title":"Automated Deduction - CADE-17","author":"F. Kamm\u00fcller","year":"2000","unstructured":"Kamm\u00fcller, F.: Modular reasoning in Isabelle. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, Springer, Heidelberg (2000), See also http:\/\/swt.cs.tu-berlin.de\/~flokam"},{"key":"26_CR3","unstructured":"Kamm\u00fcller, F.: Comparison of imps, pvs and larch with respect to theory treatment and modularization. Technical report, TU Berlin, Unpublished (1996), see http:\/\/swt.cs.tu-berlin.de\/~flokam"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44904-3_8","volume-title":"Typed Lambda Calculi and Applications","author":"T. Coquand","year":"2003","unstructured":"Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, Springer, Heidelberg (2003)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual (2005), See http:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf","DOI":"10.1007\/11542384_8"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative Algebra in the Mizar System. Journal of Symbolic Computation\u00a032, 143\u2013169 (2001)","journal-title":"Journal of Symbolic Computation"},{"key":"26_CR7","unstructured":"Trybulec, A.: Some Features of the Mizar Language. Technical report, ESPRIT Workshop, Torino (1993), See also http:\/\/mizar.org\/project\/trybulec93.ps"},{"issue":"3","key":"26_CR8","first-page":"365","volume":"2","author":"K. Hryniewiecki","year":"1990","unstructured":"Hryniewiecki, K.: Graphs. Formalized Mathematics\u00a02(3), 365\u2013370 (1990)","journal-title":"Formalized Mathematics"},{"issue":"3","key":"26_CR9","first-page":"297","volume":"5","author":"Y. Nakamura","year":"1996","unstructured":"Nakamura, Y., Rudnicki, P.: Vertex sequences induced by chains. Formalized Mathematics\u00a05(3), 297\u2013304 (1996)","journal-title":"Formalized Mathematics"},{"issue":"3","key":"26_CR10","first-page":"417","volume":"6","author":"Y. Nakamura","year":"1997","unstructured":"Nakamura, Y., Rudnicki, P.: Euler circuits and paths. Formalized Mathematics\u00a06(3), 417\u2013425 (1997)","journal-title":"Formalized Mathematics"},{"issue":"2","key":"26_CR11","first-page":"189","volume":"7","author":"Y. Nakamura","year":"1998","unstructured":"Nakamura, Y., Rudnicki, P.: Oriented chains. Formalized Mathematics\u00a07(2), 189\u2013192 (1998)","journal-title":"Formalized Mathematics"},{"issue":"2","key":"26_CR12","first-page":"143","volume":"11","author":"Y. Nakamura","year":"2003","unstructured":"Nakamura, Y., Chen, J.C.: The underlying principle of Dijkstra\u2019s shortest path algorithm. Formalized Mathematics\u00a011(2), 143\u2013152 (2003)","journal-title":"Formalized Mathematics"},{"issue":"3","key":"26_CR13","first-page":"237","volume":"11","author":"J.C. Chen","year":"2003","unstructured":"Chen, J.C.: Dijkstra\u2019s shortest path algorithm. Formalized Mathematics\u00a011(3), 237\u2013248 (2003)","journal-title":"Formalized Mathematics"},{"key":"26_CR14","unstructured":"Byli\u0144ski, C., Rudnicki, P.: The correspondence between monotonic many sorted signatures and well-founded graphs. Part I. Journal of Formalized Mathematics, vol. 8 (1996)"},{"key":"26_CR15","unstructured":"Byli\u0144ski, C., Rudnicki, P.: The correspondence between monotonic many sorted signatures and well-founded graphs. Part II. Journal of Formalized Mathematics, vol. 8 (1996)"},{"key":"26_CR16","unstructured":"Toda, Y.: The formalization of simple graphs. Journal of Formalized Mathematics, vol. 6 (1994)"},{"issue":"2","key":"26_CR17","first-page":"279","volume":"13","author":"G. Lee","year":"2005","unstructured":"Lee, G.: Weighted and labeled graphs. Formalized Mathematics\u00a013(2), 279\u2013293 (2005)","journal-title":"Formalized Mathematics"},{"issue":"2","key":"26_CR18","first-page":"295","volume":"13","author":"G. Lee","year":"2005","unstructured":"Lee, G., Rudnicki, P.: Correctness of Dijkstra\u2019s shortest path and Prim\u2019s minimum spanning tree algorithms. Formalized Mathematics\u00a013(2), 295\u2013304 (2005)","journal-title":"Formalized Mathematics"},{"issue":"2","key":"26_CR19","first-page":"235","volume":"13","author":"G. Lee","year":"2005","unstructured":"Lee, G., Rudnicki, P.: Alternative graph structures. Formalized Mathematics\u00a013(2), 235\u2013252 (2005)","journal-title":"Formalized Mathematics"},{"issue":"2","key":"26_CR20","first-page":"253","volume":"13","author":"G. Lee","year":"2005","unstructured":"Lee, G.: Walks in graphs. Formalized Mathematics\u00a013(2), 253\u2013269 (2005)","journal-title":"Formalized Mathematics"},{"issue":"2","key":"26_CR21","first-page":"271","volume":"13","author":"G. Lee","year":"2005","unstructured":"Lee, G.: Trees and graph components. Formalized Mathematics\u00a013(2), 271\u2013277 (2005)","journal-title":"Formalized Mathematics"},{"key":"26_CR22","unstructured":"Lee, G.: Verification of Graph Algorithms in Mizar. Master\u2019s thesis, University of Alberta, Dept. of Comp. Sci. (2004) See also http:\/\/www.cs.ualberta.ca\/~piotr\/Mizar"},{"issue":"2","key":"26_CR23","first-page":"305","volume":"13","author":"G. Lee","year":"2005","unstructured":"Lee, G.: Correctnesss of Ford-Fulkerson\u2019s maximum flow algorithm. Formalized Mathematics\u00a013(2), 305\u2013314 (2005)","journal-title":"Formalized Mathematics"},{"key":"26_CR24","unstructured":"Arneson, B.: Mizar Verification of Algorithms for Recognizing Chordal Graphs. Master\u2019s thesis, University of Alberta, Dept. of Comp. Sci. (2007), See also http:\/\/www.cs.ualberta.ca\/~piotr\/Mizar"},{"key":"26_CR25","volume-title":"Algorithmic Graph Theory and Perfect Graphs","author":"M.C. Golumbic","year":"1980","unstructured":"Golumbic, M.C.: Algorithmic Graph Theory and Perfect Graphs. Academic Press, New York (1980)"},{"issue":"3","key":"26_CR26","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1137\/0213035","volume":"13","author":"R.E. Tarjan","year":"1984","unstructured":"Tarjan, R.E., Yannakakis, M.: Simplie linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM Journal of Computing\u00a013(3), 566\u2013569 (1984)","journal-title":"SIAM Journal of Computing"},{"issue":"3","key":"26_CR27","doi-asserted-by":"publisher","first-page":"79","DOI":"10.2478\/v10037-006-0010-3","volume":"14","author":"B. Arneson","year":"2006","unstructured":"Arneson, B., Rudnicki, P.: Chordal graphs. Formalized Mathematics\u00a014(3), 79\u201392 (2006)","journal-title":"Formalized Mathematics"},{"issue":"4","key":"26_CR28","doi-asserted-by":"publisher","first-page":"187","DOI":"10.2478\/v10037-006-0022-z","volume":"14","author":"B. Arneson","year":"2006","unstructured":"Arneson, B., Rudnicki, P.: Recognizing chordal graphs: Lex BFS and MCS. Formalized Mathematics\u00a014(4), 187\u2013205 (2006)","journal-title":"Formalized Mathematics"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:47Z","timestamp":1619517587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}