{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:49:47Z","timestamp":1725475787723},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_30","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"401-405","source":"Crossref","is-referenced-by-count":7,"title":["System Description: IVY"],"prefix":"10.1007","author":[{"given":"William","family":"McCune","sequence":"first","affiliation":[]},{"given":"Olga","family":"Shumsky","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","key":"30_CR1","unstructured":"Kaufmann, M., Manolios, P., Moore, J. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic, Dordrecht (2000) (to appear)"},{"issue":"4","key":"30_CR2","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.: An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering\u00a023(4), 203\u2013213 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"30_CR3","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Tech. Report ANL\/MCS-TM-194, Argonne National Laboratory, Argonne, IL (May 1994)"},{"key":"30_CR4","unstructured":"McCune, W.: EQP (1994), http:\/\/www.mcs.anl.gov\/~AR\/eqp\/"},{"key":"30_CR5","unstructured":"McCune, W.: MACE: Models and Counterexamples (1994), http:\/\/www.mcs.anl.gov\/AR\/mace\/"},{"key":"30_CR6","unstructured":"McCune, W.: Otter (1994), http:\/\/www.mcs.anl.gov\/AR\/otter\/"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94\/6, Argonne National Laboratory, Argonne, IL (1994)","DOI":"10.2172\/10129052"},{"key":"30_CR8","first-page":"71","volume-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos","author":"W. McCune","year":"1997","unstructured":"McCune, W.: 33 basic test problems: A practical evaluation of some paramodulation strategies. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, ch. 5, pp. 71\u2013114. MIT Press, Cambridge (1997)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"McCune, W., Shumsky, O.: IVY: A preprocessor and proof checker for first-order logic. Preprint ANL\/MCS-P775-0899, Argonne National Laboratory, Argonne, IL (1999); To appear in [1]","DOI":"10.1007\/978-1-4757-3188-0_16"},{"issue":"2","key":"30_CR10","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W. McCune","year":"1997","unstructured":"McCune, W., Wos, L.: Otter: The CADE-13 competition incarnations. J. Automated Reasoning\u00a018(2), 211\u2013220 (1997)","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T07:10:15Z","timestamp":1683702615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/10721959_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}