{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214637,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_14","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"203-220","source":"Crossref","is-referenced-by-count":25,"title":["Three Tactic Theorem Proving"],"prefix":"10.1007","author":[{"given":"Don","family":"Syme","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"14_CR1","unstructured":"Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, Baco Raton, Florida, 1995."},{"key":"14_CR2","unstructured":"M.J.C Gordon and T.F Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"14_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL","author":"J. Harrison","year":"1996","unstructured":"J. Harrison. A Mizar Mode for HOL. In J. Von Wright, J. Grundy, and J. Harrison, editors, Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL, volume 1125 of Lecture Notes in Computer Science, pages 203\u2013220, Turku, Finland, August 1996. Springer Verlag."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Matt Kaufmann and J. Strother Moore. ACL2: An industrial strength version of Nqthm. COMPASS \u2014 Proceedings of the Annual Conference on Computer Assurance, pages 23\u201334, 1996. IEEE catalog number 96CH35960.","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"A Mechanized Logic of Computation","author":"M.J.C. Gordon","year":"1979","unstructured":"M.J.C. Gordon, R. Milner, and C.P. Wadsworth. A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1979."},{"key":"14_CR6","unstructured":"Michael Norrish. C Formalized in HOL. PhD thesis, University of Cambridge, August 1998."},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994."},{"key":"14_CR8","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1979."},{"key":"14_CR9","unstructured":"P. Rudnicki. An overview of the MIZAR project, 1992. Unpublished; available by anonymous FTP from http:\/\/www.menaik.cs.ualberta.ca as http:\/\/www.pub\/Mizar\/Mizar_Over.tar.Z ."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Don Syme. Interaction for Declarative Theorem Proving, December 1998. Available from http:\/\/research.microsoft.com\/users\/dsyme .","DOI":"10.1007\/3-540-48256-3_14"},{"key":"14_CR11","unstructured":"Don Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, Computer Laboratory, January 1999. Available from http:\/\/research.microsoft.com\/users\/dsyme ."}],"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\/3-540-48256-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T03:46:22Z","timestamp":1737344782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}