{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T05:23:36Z","timestamp":1749792216110},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_13","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T10:49:52Z","timestamp":1187779792000},"page":"157-172","source":"Crossref","is-referenced-by-count":1,"title":["Improving the Usability of HOL Through Controlled Automation Tactics"],"prefix":"10.1007","author":[{"given":"Eunsuk","family":"Kang","sequence":"first","affiliation":[]},{"given":"Mark D.","family":"Aagaard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/3-540-36126-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M.D. Aagaard","year":"2002","unstructured":"Aagaard, M.D., Day, N.A., Lou, M.: Relating multi-step and single-step microprocessor correctness statements. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 123\u2013141. Springer, Heidelberg (2002)"},{"key":"13_CR2","first-page":"46","volume-title":"Theorem Proving in Higher Order Logics","author":"P.E. Black","year":"1995","unstructured":"Black, P.E., Windley, P.J.: Automatically synthesized term denotation predicates: A proof aid. In: Theorem Proving in Higher Order Logics, pp. 46\u201357. Springer, Heidelberg (1995)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-45685-6_12","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Delahaye","year":"2002","unstructured":"Delahaye, D.: Free-style theorem proving. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 164\u2013181. Springer, Heidelberg (2002)"},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","key":"13_CR4","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York (1993)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 203\u2013220. Springer, Heidelberg (1996)"},{"key":"13_CR6","unstructured":"Harrison, J.: The HOL light system reference (2006), http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/reference_220.pdf"},{"key":"13_CR7","first-page":"154","volume-title":"BRA Types workshop","author":"J.R. Harrison","year":"1996","unstructured":"Harrison, J.R.: Proof style. In: BRA Types workshop, pp. 154\u2013172. Springer, Heidelberg (1996)"},{"key":"13_CR8","unstructured":"Hickey, J.J.: The MetaPRL Logical Programming Environment. PhD thesis, Cornell (2001)"},{"issue":"4","key":"13_CR9","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/BF01213535","volume":"8","author":"A.P. Martin","year":"1996","unstructured":"Martin, A.P., Gardiner, P.H.B., Woodcock, J.C.P.: A tactical calculus. Formal Aspects of Computing\u00a08(4), 479\u2013489 (1996)","journal-title":"Formal Aspects of Computing"},{"issue":"3-4","key":"13_CR10","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Rudnicki, P., Trybulec, A.: On equivalents of well-foundedness. Jour. of Automated Reasoning\u00a023(3-4), 197\u2013234 (1999)","journal-title":"Jour. of Automated Reasoning"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Toyn, I.: A tactic language for reasoning about z specifications. In: 3rd BCS-FACS Northern Formal Methods Workshop (September 1998)","DOI":"10.14236\/ewic\/NFM1998.16"},{"key":"13_CR12","first-page":"26","volume-title":"Int\u2019l Joint Conf. on Artificial Intelligence","author":"A. Trybulec","year":"1985","unstructured":"Trybulec, A., Blair, H.A.: Computer assisted reasoning with MIZAR. In: Int\u2019l Joint Conf. on Artificial Intelligence, pp. 26\u201328. Morgan Kaufmann, San Francisco (1985)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2013 A generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013183. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:23:02Z","timestamp":1605745382000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}