{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:26:39Z","timestamp":1764782799252,"version":"3.41.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"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":[[2002,6]]},"DOI":"10.1023\/a:1021693818601","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T02:03:09Z","timestamp":1048212189000},"page":"107-124","source":"Crossref","is-referenced-by-count":4,"title":["Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus"],"prefix":"10.1007","volume":"29","author":[{"given":"Larry","family":"Wos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dolph","family":"Ulrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Branden","family":"Fitelson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5110710_CR1","first-page":"173","volume":"1","author":"N. Belnap","year":"1976","unstructured":"Belnap, N.: The two-property, Relevance Logic Newsletter\n1(1976), 173-180.","journal-title":"Relevance Logic Newsletter"},{"key":"5110710_CR2","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1023\/A:1005731217123","volume":"20","author":"K. Hodgson","year":"1998","unstructured":"Hodgson, K.: Shortest single axioms for the equivalential calculus with CD and RCD, J. Automated Reasoning\n20(1998), 283-316.","journal-title":"J. Automated Reasoning"},{"key":"5110710_CR3","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1305\/ndjfl\/1093888216","volume":"19","author":"J. A. Kalman","year":"1978","unstructured":"Kalman, J. A.: A shortest single axiom for the classical equivalential calculus, Notre Dame J. Formal Logic\n19(1978), 141-144.","journal-title":"Notre Dame J. Formal Logic"},{"key":"5110710_CR4","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF00370343","volume":"41","author":"J. A. Kalman","year":"1982","unstructured":"Kalman, J. A.: The two-property and condensed detachment, Studia Logica\n41(1982), 173-179.","journal-title":"Studia Logica"},{"key":"5110710_CR5","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/BF01371632","volume":"42","author":"J. A. Kalman","year":"1983","unstructured":"Kalman, J. A.: Condensed detachment as a rule of inference, Studia Logica\n42(1983), 443-451.","journal-title":"Studia Logica"},{"key":"5110710_CR6","volume-title":"Selected Works","author":"J. Lukasiewicz","year":"1970","unstructured":"Lukasiewicz, J.: Selected Works, edited by L. Borokowski, North-Holland, Amsterdam, 1970."},{"key":"5110710_CR7","doi-asserted-by":"crossref","DOI":"10.2172\/10129052","volume-title":"OTTER 3.0 reference manual and guide, Tech. Report ANL-94\/6","author":"W. McCune","year":"1994","unstructured":"McCune, W.: OTTER 3.0 reference manual and guide, Tech. Report ANL-94\/6, Argonne National Laboratory, Argonne, IL, 1994."},{"issue":"3","key":"5110710_CR8","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1305\/ndjfl\/1093957574","volume":"4","author":"C. A. Meredith","year":"1963","unstructured":"Meredith, C. A. and Prior, A.: Notes on the axiomatics of the propositional calculus, Notre Dame J. Formal Logic\n4(3) (1963), 171-187.","journal-title":"Notre Dame J. Formal Logic"},{"unstructured":"Peterson, J. G.: The possible shortest single axioms for EC-tautologies, Report 105, Department of Mathematics, University of Auckland, 1977.","key":"5110710_CR9"},{"unstructured":"Thiele, R. and Wos, L.: Hilbert's twenty-fourth problem, J. Automated Reasoning, to appear.","key":"5110710_CR10"},{"issue":"3","key":"5110710_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-239.","journal-title":"J. Automated Reasoning"},{"key":"5110710_CR12","first-page":"205","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 for the equivalential calculus: An application of automated theorem proving to infinite domains, Notre Dame J. Formal Logic\n24(1983), 205-223.","journal-title":"Notre Dame J. Formal Logic"},{"key":"5110710_CR13","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\n6(1990), 213-232.","journal-title":"J. Automated Reasoning"},{"key":"5110710_CR14","doi-asserted-by":"crossref","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning","author":"L. Wos","year":"1999","unstructured":"Wos, L. and Pieper, G. W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific, Singapore, 1999."},{"unstructured":"Wos, L.: The strategy of cramming, J. Automated Reasoning, accepted.","key":"5110710_CR15"},{"unstructured":"Wos, L., Ulrich, D. and Fitelson, B.: XCB, the last of the shortest single axioms for the classical equivalential calculus, Bulletin of the Section on Logic, accepted.","key":"5110710_CR16"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021693818601.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021693818601\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021693818601.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:23:50Z","timestamp":1749122630000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021693818601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["5110710"],"URL":"https:\/\/doi.org\/10.1023\/a:1021693818601","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}