{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:50Z","timestamp":1742617190602,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_77","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:06:31Z","timestamp":1330279591000},"page":"369-384","source":"Crossref","is-referenced-by-count":8,"title":["Formalization of planar graphs"],"prefix":"10.1007","author":[{"given":"Mitsuharu","family":"Yamamoto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shin-ya","family":"Nishizaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masami","family":"Hagiya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yozo","family":"Toda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Ching-Tsun Chou. A formal theory of undirected graphs in higher-order logic. In Thomas F. Melham and Juanito Camilleri, editors, 7th International Workshop on Higher-Order Logic Theorem Proving System and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 144\u2013157. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_40"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Ching-Tsun Chou. Mechanical verification of distributed algorithms in higher-order logic. In Thomas F. Melham and Juanito Camilleri, editors, 7th International Workshop on Higher-Order Logic Theorem Proving System and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 158\u2013176. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_41"},{"key":"25_CR3","series-title":"Addison-Wesley series in mathematics","doi-asserted-by":"crossref","DOI":"10.21236\/AD0705364","volume-title":"Graph theory","author":"F. Harary","year":"1969","unstructured":"Frank Harary. Graph theory. Addison-Wesley series in mathematics. Addison-Wesley, London, 1969."},{"key":"25_CR4","unstructured":"Thomas F. Melham. The HOL sets Library. University of Cambridge, Computer Laboratory, October 1991."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Thomas F. Melham. A package for inductive relation definition in HOL. In Proceedings of the 1991 International Tutorial and Workshop on the HOL Theorem Proving System, pages 27\u201330. IEEE Computer Society Press, August 1991.","DOI":"10.1109\/HOL.1991.596299"},{"key":"25_CR6","volume-title":"Number 3 in Information Mathematics Lectures","author":"S. Negami","year":"1993","unstructured":"Seiya Negami. Discrete Structures. Number 3 in Information Mathematics Lectures. Kyouritsu Shuppan, Tokyo, Japan, May 1993. (in Japanese)."},{"key":"25_CR7","unstructured":"University of Cambridge, Computer Laboratory. The HOL System: DESCRIPTION, March 1994."},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Jan van Leeuwen. Graph Algorithms, volume A of Handbook of Theoretical Computer Science, chapter 10, pages 525\u2013633. MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50015-1"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Wai Wong. A simple graph theory and its application in railway signaling. In M. Archer et al., editor, Proc. of 1991 Workshop on the HOL Theorem Proving System and Its Applications, pages 395\u2013409. IEEE Computer Society Press, 1992.","DOI":"10.1109\/HOL.1991.596304"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_77.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:57:56Z","timestamp":1742597876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_77"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_77","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}