{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:03Z","timestamp":1725664923197},"publisher-location":"Berlin, Heidelberg","reference-count":15,"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_56","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:06:11Z","timestamp":1330261571000},"page":"46-57","source":"Crossref","is-referenced-by-count":4,"title":["Automatically synthesized term denotation predicates: A proof aid"],"prefix":"10.1007","author":[{"given":"Paul E.","family":"Black","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phillip J.","family":"Windley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"4_CR1","unstructured":"Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley Publishing Co., 1986."},{"key":"4_CR2","unstructured":"Jim Alves-Foss. message of 1 November 1991 to info-hol mailing list. (Available electronically at http:\/\/lal.cs.byu.edu\/lal\/hol-documentation.html)"},{"key":"4_CR3","first-page":"9","volume-title":"Machine Learning. An Artificial Intelligence Approach","year":"1983","unstructured":"Jaime G. Carbonell, Ryszard S. Michalski, and Tom M. Mitchell. (Eds.) Machine Learning. An Artificial Intelligence Approach. Tioga Publishing Company, Palo Alto, California, 94302, 1983, page 9."},{"key":"4_CR4","unstructured":"Eugene Charniak, Christopher K. Riesbeck, and Drew V. McDermott. Artificial Intelligence Programming. Lawrence Erlbaum Associates, 1980, chapters 11 and 14, pp. 121\u2013130 and 162\u2013176."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ching-Tsun Chou. \u201cA Note on Interactive Theorem Proving with Theorem Continuation Functions,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL '92), edited by Luc Claesen and Michael Gordon, Elsevier Science Publishers B.V., 1992, pp. 59\u201369.","DOI":"10.1016\/B978-0-444-89880-7.50010-3"},{"key":"4_CR6","unstructured":"Paul Curzon. Re: Accessing Assumptions. message of 25 May 1994 to hol2000 mailing list. (Available electronically at http:\/\/lal.cs.byu.edu\/lal\/holdocumentation.html)"},{"key":"4_CR7","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL. A theorem proving environment for higher order logic. Cambridge University Press, 1993, Section 24.5, pp. 384\u2013396."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Cao Feng and Stephen Muggleston. \u201cTowards Inductive Generalisation in Higher Order Logic,\u201d in Machine Learning: Proceedings of the Ninth International Workshop (ML92) edited by Derek Sleeman and Peter Edwards, Morgan Kaufmann Publishers, 1992, pp. 154\u2013162.","DOI":"10.1016\/B978-1-55860-247-2.50025-5"},{"key":"4_CR9","unstructured":"John Harrison. Selecting Assumptions. message of 31 October 1991 to info-hol mailing list. (Available electronically at http:\/\/lal.cs.byu.edu\/lal\/holdocumentation.html)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Sara Kalvala, Myla Archer, Karl Levitt. \u201cImplementation and Use of Annotations in HOL,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL '92), edited by Luc Claesen and Michael Gordon, Elsevier Science Publishers B.V., 1992, pp. 407\u2013426.","DOI":"10.1016\/B978-0-444-89880-7.50032-2"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Kenji Kira and Larry A. Rendell. \u201cA Practical Approach to Feature Selection,\u201d in Machine Learning: Proceedings of the Ninth International Workshop (ML92) edited by Derek Sleeman and Peter Edwards, Morgan Kaufmann Publishers, 1992, pp. 249\u2013256.","DOI":"10.1016\/B978-1-55860-247-2.50037-1"},{"key":"4_CR12","unstructured":"Miriam Leeser. assumption numbering, user interfaces .... message of 26 May 1994 to hol2000 mailing list, archived at http:\/\/lal.cs.byu.edu\/lal\/holdocumentation.html."},{"key":"4_CR13","unstructured":"David Shepherd. Re: Accessing Assumptions. message of 26 May 1994 to hol2000 mailing list. (Available electronically at http:\/\/lal.cs.byu.edu\/lal\/holdocumentation.html)"},{"key":"4_CR14","unstructured":"Steven L. Tanimoto. The Elements of Artificial Intelligence. Computer Science Press, 1987."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley and Michael Coe. \u201cA Correctness Model for Pipelined Microprocessors,\u201d in Proceedings of the 1994 Conference on Theorem Provers in Circuit Design, edited by Thomas Kropf and Ramayya Kumar, 1994.","DOI":"10.1007\/3-540-59047-1_41"}],"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_56.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:57:16Z","timestamp":1605628636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}