{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T12:11:35Z","timestamp":1780315895822,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540649878","type":"print"},{"value":"9783540498018","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055153","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"479-496","source":"Crossref","is-referenced-by-count":8,"title":["Formalization of graph search algorithms and its applications"],"prefix":"10.1007","author":[{"given":"Mitsuharu","family":"Yamamoto","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Koichi","family":"Takahashi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Masami","family":"Hagiya","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shin-ya","family":"Nishizaki","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tetsuo","family":"Tamai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"David Basin and Matt Kaufmann. The Boyer-Moore prover and Nuprl: An experimental comparison. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 89\u2013119. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.006"},{"key":"28_CR2","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, New York, 1979."},{"key":"28_CR3","unstructured":"Albert J. Camilleri and Wishnu Prasetya. Cpo theory, 1994. Available from http:\/\/www.cl.cam.ac.uk\/ftp\/hvg\/hol88\/contrib\/cpo\/."},{"key":"28_CR4","first-page":"144","volume-title":"volume 859 of LNCS","author":"C.-T. Chou","year":"1994","unstructured":"C.-T. Chou. A formal theory of undirected graphs in higher-order logic. In Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 859 of LNCS, pages 144\u2013157, Valletta, Malta, September 1994. Springer-Verlag."},{"key":"28_CR5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-61042-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Chou","year":"1996","unstructured":"Ching-Tsun Chou and Doron Peled. Verifying a model-checking algorithm. In Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in LNCS, pages 241\u2013257, Passau, Germany, 1996. Springer-Verlag."},{"key":"28_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"28_CR7","unstructured":"E. Allen Emerson. Handbook of Theoretical Computer Science, chapter 16. Elsevier Science Publishers B.V., 1990."},{"key":"28_CR8","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"28_CR9","first-page":"306","volume-title":"number 230 in LNCS","author":"R. H\u00c4hnle","year":"1986","unstructured":"R. H\u00c4hnle, M. Heisel, W. Reif, and W. Stephan. An interactive verification system based on dynamic logic. In J. Seikmann, editor, 8th International Conference on Automated Deduction, number 230 in LNCS, pages 306\u2013315, Oxford, 1986. Springer-Verlag. Also note etsehttp:\/\/www.informatik.uni-ulm.de\/pm\/kiv\/kiv.htmletse."},{"key":"28_CR10","unstructured":"Wim H. Hesselink. The verified incremental design of a distributed spanning tree algorithm \u2014 extended abstract. Computing Science Reports Groningen CS-R9602, November 1997. Available from http:\/\/www.cs.rug.nl\/~wim\/ghs\/whh168.ps."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"G. Kildall. A unified approach to global program optimization. In POPL, pages 194\u2013206, 1973.","DOI":"10.1145\/512927.512945"},{"key":"28_CR12","unstructured":"Bruno Martin, July 1997. Private Communication."},{"key":"28_CR13","unstructured":"Nils J. Nilsson. Principles of Artificial Intelligence. Tioga Publishing, 1980."},{"key":"28_CR14","unstructured":"N. Shankar, S. Owre, and J. Rushby. The PVS proof checker: A reference manual. Technical report, Computer Science Lab, SRI Intl., 1993."},{"key":"28_CR15","unstructured":"Tetsuo Tamai. A class of fixed-point problems on graphs and iterative solution algorithms. In Logic and Software Engineering, pages 102\u2013121. World Scientific, 1996."},{"key":"28_CR16","first-page":"197","volume-title":"volume A-20 of IFIP Transactions","author":"P. Windley","year":"1992","unstructured":"P. Windley. Abstract theories in HOL. In Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10\/WG10.2 Workshop, volume A-20 of IFIP Transactions, pages 197\u2013210, Leuven, Belgium, September 1992. North-Holland\/Elsevier."},{"key":"28_CR17","first-page":"395","volume-title":"A simple graph theory and its application in railway signalling","author":"W. Wong","year":"1992","unstructured":"W. Wong. A simple graph theory and its application in railway signalling. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 395\u2013409, Davis, California, USA, August 1991. IEEE Computer Society Press, 1992."},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Mitsuharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya, and Yozo Toda. Formalization of planar graphs. In 8th International Workshop on Higher-Order Logic Theorem Proving and Its Applications, volume 971 of LNCS, pages 369\u2013384. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_77"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:33:57Z","timestamp":1555749237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0055153","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}