{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T20:24:58Z","timestamp":1765484698265,"version":"3.41.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,8,1]],"date-time":"2001-08-01T00:00:00Z","timestamp":996624000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,8,1]],"date-time":"2001-08-01T00:00:00Z","timestamp":996624000000},"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":[[2001,8]]},"DOI":"10.1023\/a:1010639725972","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T03:31:49Z","timestamp":1040614309000},"page":"157-174","source":"Crossref","is-referenced-by-count":18,"title":["Solving Open Questions and Other Challenge Problems Using Proof Sketches"],"prefix":"10.1007","volume":"27","author":[{"given":"Robert","family":"Veroff","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"323441_CR1","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF02341853","volume":"8","author":"D. Barker-Plummer","year":"1992","unstructured":"Barker-Plummer, D.: Gazing: An approach to the problem of definition and lemma use, J. Automated Reasoning\n8(3) (1992), 311-344.","journal-title":"J. Automated Reasoning"},{"key":"323441_CR2","volume-title":"MCC Tech. Report AI-2158-86","author":"W. Bledsoe","year":"1986","unstructured":"Bledsoe, W.: The use of analogy in proof discovery, MCC Tech. Report AI-2158-86, Microelectronics and Computer Technology Corporation, Austin, Texas, 1986."},{"key":"323441_CR3","doi-asserted-by":"crossref","unstructured":"Brock, B., Cooper, S., and Pierce, W.: Analogical reasoning and proof discovery, in E. Lusk and R. Overbeek (eds.), Proc. of the 9th International Conference on Automated Deduction, Lecture Notes in Comput. Sci. 310, Springer-Verlag, 1988, pp. 454-468.","DOI":"10.1007\/BFb0012849"},{"issue":"23","key":"323441_CR4","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","volume":"57","author":"F. Giunchiglia","year":"1992","unstructured":"Giunchiglia, F. and Walsh T.: A theory of abstraction, Artificial Intelligence\n57(2, 3) (1992), 323-389.","journal-title":"Artificial Intelligence"},{"key":"323441_CR5","first-page":"1","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., and Wos, L.: Complexity and related enhancements for automated theorem-proving programs, Comput. Math. Appl.\n2 (1976), 1-16.","journal-title":"Comput. Math. Appl."},{"key":"323441_CR6","volume-title":"Technical Report ANL-94\/6","author":"W. McCune","year":"1994","unstructured":"McCune, W.: OTTER 3.0 reference manual and guide, Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, IL, 1994."},{"key":"323441_CR7","first-page":"266","volume":"10","author":"C. Meredith","year":"1969","unstructured":"Meredith, C.: Equational postulates for the Sheffer stroke, Notre Dame J. Formal Logic\n10 (1969), 266-270.","journal-title":"Notre Dame J. Formal Logic"},{"key":"323441_CR8","doi-asserted-by":"crossref","unstructured":"Plaisted, D.: Abstraction mappings in mechanical theorem proving, in W. Bibel and R. Kowalski (eds.), Proc. of the 5th International Conference on Automated Deduction, Lecture Notes in Comput. Sci. 87, Springer-Verlag, 1980, pp. 264-280.","DOI":"10.1007\/3-540-10009-1_21"},{"key":"323441_CR9","first-page":"227","volume":"1","author":"J. Robinson","year":"1965","unstructured":"Robinson, J.: Automatic deduction with hyper-resolution, International J. Comput. Math.\n1 (1965), 227-234.","journal-title":"International J. Comput. Math."},{"key":"323441_CR10","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0004-3702(74)90026-5","volume":"5","author":"E. Sacerdoti","year":"1974","unstructured":"Sacerdoti, E.: Planning in a hierarchy of abstraction spaces, Artificial Intelligence\n5 (1974), 115-135.","journal-title":"Artificial Intelligence"},{"key":"323441_CR11","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1090\/S0002-9947-1913-1500960-1","volume":"14","author":"H. Sheffer","year":"1913","unstructured":"Sheffer, H.: A set of five independent postulates for Boolean algebras, with application to logical constants, Trans. Amer. Math. Soc.\n14 (1913), 481-488.","journal-title":"Trans. Amer. Math. Soc."},{"key":"323441_CR12","volume-title":"Technical Report ANL-81\/6","author":"R. Veroff","year":"1981","unstructured":"Veroff, R.: Canonicalization and demodulation, Technical Report ANL-81\/6, Argonne National Laboratory, Argonne, IL, 1981."},{"issue":"2","key":"323441_CR13","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00244283","volume":"8","author":"R. Veroff","year":"1992","unstructured":"Veroff, R. and Wos, L.: The linked inference principle, I: The formal treatment, J. Automated Reasoning\n8(2) (1992), 213-274.","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"323441_CR14","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-239.","journal-title":"J. Automated Reasoning"},{"key":"323441_CR15","volume-title":"Technical Report TRCS-20","author":"R. Veroff","year":"2000","unstructured":"Veroff, R.: Axiom systems for Boolean algebra using the Sheffer stroke, Technical Report TRCS-20, Computer Science Department, University of New Mexico, Albuquerque, New Mexico, 2000."},{"key":"323441_CR16","volume-title":"Technical Report TR-CS-25","author":"R. Veroff","year":"2000","unstructured":"Veroff, R.: Short 2-bases for Boolean algebra in terms of the Sheffer stroke, Technical Report TR-CS-25, Computer Science Department, University of New Mexico, Albuquerque, New Mexico, 2000."},{"key":"323441_CR17","unstructured":"Veroff, R.: http:\/\/www.cs.unm.edu\/~veroff\/BA\/, 2000."},{"key":"323441_CR18","unstructured":"Wolfram, S.: Correspondence by electronic mail, February 4, 2000."},{"key":"323441_CR19","unstructured":"Wolfram, S.: A new kind of science, http:\/\/wolframscience.com, 2000."},{"key":"323441_CR20","doi-asserted-by":"crossref","unstructured":"Wos, L., Veroff, R., Smith, B., and McCune, W.: in R. Shostak (ed.), The Linked Inference Principle, II: The User's Viewpoint, Proc. of the 7th International Conference on Automated Deduction, Lecture Notes in Comput. Sci. 170, Springer-Verlag, 1984, pp. 316-332.","DOI":"10.1007\/978-0-387-34768-4_19"},{"key":"323441_CR21","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 R. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, Dordrecht, 1991, pp. 297-345."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010639725972.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1010639725972\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010639725972.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:31:38Z","timestamp":1749123098000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1010639725972"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,8]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,8]]}},"alternative-id":["323441"],"URL":"https:\/\/doi.org\/10.1023\/a:1010639725972","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2001,8]]}}}