{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:52Z","timestamp":1749125152470},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf00881802","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T02:42:21Z","timestamp":1104115341000},"page":"279-315","source":"Crossref","is-referenced-by-count":13,"title":["Searching for circles of pure proofs"],"prefix":"10.1007","volume":"15","author":[{"given":"Larry","family":"Wos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","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 19 (1978), 141?144.","journal-title":"Notre Dame J. Formal Logic"},{"key":"CR2","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 42 (1983), 443?451.","journal-title":"Studia Logica"},{"key":"CR3","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,Computers and Mathematics with Applications 2 (1976), 1?16.","journal-title":"Computers and Mathematics with Applications"},{"key":"CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"209","volume-title":"Proc. 11th Int. Conf. on Automated Deduction (CADE-11)","author":"W. McCune","year":"1992","unstructured":"McCune, W. and Wos, L.: Experiments in automated deduction with condensed detachment, in D. Kapur (ed.),Proc. 11th Int. Conf. on Automated Deduction (CADE-11), Lecture Notes in Artificial Intelligence, 607, Springer-Verlag, New York, 1992, pp. 209?223."},{"key":"CR5","unstructured":"McCune, W.:Otter 3.0, Preprint MCS-P399-1193, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, November 1993."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1305\/ndjfl\/1093887534","volume":"17","author":"J. Peterson","year":"1976","unstructured":"Peterson, J.: Shortest single axioms for the equivalential calculus,Notre Dame J. Formal Logic 17 (1976), 267?271.","journal-title":"Notre Dame J. Formal Logic"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1305\/ndjfl\/1093870311","volume":"24","author":"L. Wos","year":"1983","unstructured":"Wos, L., Winker, S., Veroff, R., Smith, B., and Henschen, L.: Questions concerning possible shortest single axioms in equivalential calculus: An application of automated theorem proving to infinite domains,Notre Dame J. Formal Logic 24 (1983) 205?223.","journal-title":"Notre Dame J. Formal Logic"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0004-3702(84)90054-7","volume":"22","author":"L. Wos","year":"1984","unstructured":"Wos, L., Winker, S., Veroff, R., Smith, B., and Henschen, L.: A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains,Artificial Intelligence 22 (1984), 303?356.","journal-title":"Artificial Intelligence"},{"key":"CR9","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1987","unstructured":"Wos, L.:Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, NJ, 1987."},{"issue":"2","key":"CR10","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00245821","volume":"6","author":"L. Wos","year":"1990","unstructured":"Wos, L.: Meeting the challenge of fifty years of logic,J. Automated Reasoning 6(2) (1990), 213?222.","journal-title":"J. Automated Reasoning"},{"key":"CR11","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1992","unstructured":"Wos, L., Overbeek, R., Lusk, E., and Boyle, J.:Automated Reasoning: Introduction and Applications, 2nd edn, McGraw-Hill, New York, 1992.","edition":"2nd edn"},{"key":"CR12","unstructured":"Wos, L.: Personal information, Argonne National Laboratory, 1994."},{"key":"CR13","volume-title":"Automating the Search for Elegant Proofs: An Experimenter's Notebook","author":"L. Wos","year":"1995","unstructured":"Wos, L.:Automating the Search for Elegant Proofs: An Experimenter's Notebook. Academic Press, San Diego, CA, 1995 (to appear)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881802.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881802\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881802","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T08:58:10Z","timestamp":1556528290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":13,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881802"],"URL":"https:\/\/doi.org\/10.1007\/bf00881802","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}