{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:50:19Z","timestamp":1761922219632,"version":"build-2065373602"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,10]]},"DOI":"10.1023\/a:1005847113370","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"135-175","source":"Crossref","is-referenced-by-count":5,"title":["Automating the Search for Elegant Proofs"],"prefix":"10.1007","volume":"21","author":[{"given":"Larry","family":"Wos","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"145691_CR1","series-title":"Lecture Notes in Artificial Intelligence","first-page":"462","volume-title":"Proc. CADE-11","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lunch, C. and Snyder, W.: Basic paramodulation and superposition, in Proc. CADE-11, Lecture Notes in Artificial Intelligence Vol. 607, D. Kapur (ed.), Springer-Verlag, Berlin, 1992, pp. 462\u2013476."},{"key":"145691_CR2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1305\/ndjfl\/1093888216","volume":"19","author":"J. Kalman","year":"1978","unstructured":"Kalman, J.: A shortest single axiom for the classical equivalential calculus, Notre Dame J. Formal Logic\n19 (1978), 141\u2013144.","journal-title":"Notre Dame J. Formal Logic"},{"key":"145691_CR3","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/BF01371632","volume":"42","author":"J. Kalman","year":"1983","unstructured":"Kalman, J.: Condensed detachment as a rule of inference, Studia Logica\n42 (1983), 443\u2013451.","journal-title":"Studia Logica"},{"key":"145691_CR4","first-page":"250","volume-title":"Jan Lukasiewicz: Selected Works","author":"J. Lukasiewicz","year":"1970","unstructured":"Lukasiewicz, J.: The equivalential calculus, in Jan Lukasiewicz: Selected Works, L. Borkowski (ed), North-Holland, Amsterdam, 1970, pp. 250\u2013277."},{"key":"145691_CR5","series-title":"Technical Report","volume-title":"OTTER 2.0 Users Guide","author":"W. McCune","year":"1990","unstructured":"McCune, W.: OTTER 2.0 Users Guide, Technical Report ANL-90\/9, Argonne National Laboratory, Argonne, Illinois, 1990."},{"key":"145691_CR6","series-title":"Technical Memorandum","volume-title":"What's New in OTTER 2.2","author":"W. McCune","year":"1991","unstructured":"McCune, W.: What's New in OTTER 2.2, Technical Memorandum ANL\/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, 1991."},{"key":"145691_CR7","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.2172\/10129052","volume-title":"OTTER 3.0 Reference Manual and Guide","author":"W. McCune","year":"1994","unstructured":"McCune, W.: OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, Illinois, 1994."},{"key":"145691_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61398-6","volume-title":"Automated Deduction in Equational Logic and Cubic Curves","author":"W. McCune","year":"1996","unstructured":"McCune, W. and Padmanabhan, R.: Automated Deduction in Equational Logic and Cubic Curves, Lecture Notes in Computer Science Vol. 1095, Springer-Verlag, Heidelberg, 1996. See http:\/\/www.mcs.anl.gov\/home\/mccune\/ar\/monograph\/ for additional information."},{"issue":"2","key":"145691_CR9","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1090\/S0002-9939-1973-0325498-2","volume":"41","author":"R. Padmanabhan","year":"1973","unstructured":"Padmanabhan, R. and Quackenbush, R. W.: Equational theories of algebras with distributive congruence, Proc. of AMS\n41(2) (1973), 373\u2013377.","journal-title":"Proc. of AMS"},{"key":"145691_CR10","unstructured":"Scott, D.: Private communication, 1990."},{"issue":"3","key":"145691_CR11","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R. Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies, J. Automated Reasoning\n16(3) (1996), 223\u2013239.","journal-title":"J. Automated Reasoning"},{"key":"145691_CR12","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-011-3488-0_15","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"L. Wos","year":"1991","unstructured":"Wos, L.: Automated reasoning and Bledsoe's dream for the field, in Automated Reasoning: Essays in Honor of Woody Bledsoe, R. S. Boyer (ed.), Kluwer Academic Publishers, Dordrecht, 1991, pp. 297\u2013345."},{"key":"145691_CR13","first-page":"3","volume-title":"Festschrift for J. A. Robinson","author":"L. Wos","year":"1991","unstructured":"Wos, L., Overbeek, R. and Lusk, E.: Subsumption, a sometimes undervalued procedure, in Festschrift for J. A. Robinson, J.-L. Lassez and G. Plotkin (eds), MIT Press, Cambridge, Mass., 1991, pp. 3\u201340."},{"key":"145691_CR14","first-page":"321","volume":"5","author":"L. Wos","year":"1992","unstructured":"Wos, L. and McCune, W.: The application of automated reasoning to questions in mathematics and logic, Annals of Mathematics and AI\n5 (1992), 321\u2013370.","journal-title":"Annals of Mathematics and AI"},{"issue":">2","key":"145691_CR15","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0898-1221(94)00220-F","volume":"29","author":"L. Wos","year":"1995","unstructured":"Wos, L.: The resonance strategy, Computers and Mathematics with Applications (special issue on automated reasoning), 29(2) (1995), 133\u2013178.","journal-title":"Computers and Mathematics with Applications"},{"issue":"3","key":"145691_CR16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF00881802","volume":"15","author":"L. Wos","year":"1995","unstructured":"Wos, L.: Searching for circles of pure proofs, J. Automated Reasoning\n15(3) (1995), 279\u2013315.","journal-title":"J. Automated Reasoning"},{"key":"145691_CR17","volume-title":"The Automation of Reasoning: An Experimenter's Notebook with OTTER Tutorial","author":"L. Wos","year":"1996","unstructured":"Wos, L.: The Automation of Reasoning: An Experimenter's Notebook with OTTER Tutorial, Academic Press, New York, 1996. See http:\/\/www.mcs.anl.gov\/people\/wos\/index.html for input files and information on shorter proofs."},{"issue":"2","key":"145691_CR18","first-page":"259","volume":"17","author":"L. Wos","year":"1996","unstructured":"Wos, L.: OTTER and the Moufang identity problem, J. Automated Reasoning\n17(2) (1996), 259\u2013289.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"145691_CR19","first-page":"23","volume":"17","author":"L. Wos","year":"1996","unstructured":"Wos, L.: The power of combining resonance with heat, J. Automated Reasoning\n17(1) (1996), 23\u201381.","journal-title":"J. Automated Reasoning"},{"key":"145691_CR20","series-title":"Tech. Memo","doi-asserted-by":"crossref","DOI":"10.2172\/516006","volume-title":"Experiments Concerning the Automated Search for Elegant Proofs","author":"L. Wos","year":"1997","unstructured":"Wos, L.: Experiments Concerning the Automated Search for Elegant Proofs, Tech. Memo ANL\/MCS-TM-221, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, 1997."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005847113370.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005847113370\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005847113370.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:39:59Z","timestamp":1749123599000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005847113370"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,10]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,10]]}},"alternative-id":["145691"],"URL":"https:\/\/doi.org\/10.1023\/a:1005847113370","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,10]]}}}