{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:25:39Z","timestamp":1764782739667,"version":"3.41.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"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,6]]},"DOI":"10.1023\/a:1005731217123","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:13:52Z","timestamp":1040512432000},"page":"283-316","source":"Crossref","is-referenced-by-count":3,"title":["Shortest Single Axioms for the Equivalential Calculus with CD and RCD"],"prefix":"10.1007","volume":"20","author":[{"given":"Kahlil","family":"Hodgson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"122366_CR1","unstructured":"Hodgson, Kahlil: Program iteration: The development of a generic driving system for\nOTTER\n. Summer Scholarship Project, University of Auckland, New Zealand, report for Summer 94\/95."},{"issue":"2","key":"122366_CR2","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1112\/jlms\/s2-14.2.193","volume":"14","author":"J. A. Kalman","year":"1976","unstructured":"Kalman, J. A.: Axiomatisations of logics with values in groups, J. London Math. Soc.\n14(2) (1976), 193\u2013199.","journal-title":"J. London Math. Soc."},{"key":"122366_CR3","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\u2013451.","journal-title":"Studia Logica"},{"key":"122366_CR4","unstructured":"Kalman, J. A.: Testing logical matrices with the help of an automated reasoning program, Proc. 17th International Symposium on Multiple-Valued Logic, Boston, Massachusetts, May 26\u201328 1987, pp. 276\u2013281."},{"key":"122366_CR5","volume-title":"Automated Reasoning with OTTER","author":"J. A. Kalman","year":"1995","unstructured":"Kalman, J. A.: Automated Reasoning with\nOTTER, Course notes for paper 26.414 at University of Auckland, New Zealand, 1995."},{"key":"122366_CR6","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1305\/ndjfl\/1093888216","volume":"19","author":"J. A. Kalman","year":"1978","unstructured":"Kalman, John A.: A shortest single axiom for the equivalential calculus, Notre Dame J. Formal Logic\n19 (1978), 141\u2013144.","journal-title":"Notre Dame J. Formal Logic"},{"key":"122366_CR7","unstructured":"Lawes, Elliot: Shortest Single Axioms for the Equivalential Calculus Using Condensed Detachment and Reversed Condensed Detachment as Inference Rules, Summer Scholarship Project, University of Auckland, New Zealand, report for Summer 94\/95."},{"key":"122366_CR8","first-page":"145","volume":"1","author":"J. \u0141ukasiewicz","year":"1939","unstructured":"\u0141ukasiewicz, J.: Der \u00c4quivalenzenkalk\u00fcl, Collectanea Logica\n1 (1939), 145\u2013169. English translation in S. McCall (ed.), Polish Logic 1920\u20131939, Oxford University Press, Oxford, 1967, pp. 88\u2013115.","journal-title":"Collectanea Logica"},{"key":"122366_CR9","unstructured":"Matlab: User's Guide (Version 4.0), The Math Works, August 1992."},{"key":"122366_CR10","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. N.: Axiomatics of the propositional calculus, Notre Dame J. Formal Logic\n4 (1963), 171\u2013187.","journal-title":"Notre Dame J. Formal Logic"},{"key":"122366_CR11","series-title":"Technical Memo","volume-title":"A Davis\u2013Putnam program and its application to finite first-order model search: Quasi-group existence problems","author":"W. W. McCune","year":"1994","unstructured":"McCune, W. W.: A Davis\u2013Putnam program and its application to finite first-order model search: Quasi-group existence problems, Technical Memo, ANL\/MCS-TM-194, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Ill., 1994."},{"key":"122366_CR12","series-title":"Technical report","doi-asserted-by":"crossref","DOI":"10.2172\/10129052","volume-title":"OTTER 3.0 Reference Manual and Guide","author":"W. W. McCune","year":"1994","unstructured":"McCune, W. W.: OTTER 3.0 Reference Manual and Guide, Technical report ANL-94\/6, Argonne National Laboratory, Argonne, Ill., January 1994."},{"key":"122366_CR13","doi-asserted-by":"crossref","unstructured":"McCune, W. and Padmanabhan, R.: Automated Deduction in Equational Logic and Geometry, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61398-6"},{"key":"122366_CR14","doi-asserted-by":"crossref","first-page":"959","DOI":"10.1090\/S0002-9904-1947-08916-3","volume":"53","author":"J. C. C. McKinsey","year":"1947","unstructured":"McKinsey, J. C. C. and Diamond, A. H.: Algebras and their sub-algebras, Bull. Amer. Math. Soc.\n53 (1947), 959\u2013962.","journal-title":"Bull. Amer. Math. Soc."},{"key":"122366_CR15","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1016\/0021-8693(75)90169-6","volume":"34","author":"N. S. Mendelsohn","year":"1975","unstructured":"Mendelsohn, N. S. and Padmanabhan, R.: Minimal identities for Boolean groups, J. Algebra\n34 (1975), 451\u2013457.","journal-title":"J. Algebra"},{"key":"122366_CR16","unstructured":"Prior, A. N.: Formal Logci, 2nd ed., Oxford University Press, 1962."},{"key":"122366_CR17","unstructured":"Peterson, J. G.: The possible shortest single axioms for EC-tautologies, Technical Report No. 105, Department of Mathematics, University of Auckland, March 1977."},{"key":"122366_CR18","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1305\/ndjfl\/1093887534","volume":"17","author":"J. G. Peterson","year":"1976","unstructured":"Peterson, J. G.: Shortest single axioms for the equivalential calculus, Notre Dame J. Formal Logic\n17 (1976), 267\u2013271.","journal-title":"Notre Dame J. Formal Logic"},{"key":"122366_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0229-2","volume-title":"The Maple Handbook: Maple V Release 3","author":"D. Redfern","year":"1994","unstructured":"Redfern, D.: The Maple Handbook: Maple V Release 3, Springer-Verlag, New York, 1994."},{"key":"122366_CR20","unstructured":"Tarski, A.: Logic, Semantics, Metamathematics: Papers from 1923 to 1938 (translated by J. H. Woodger), Oxford University Press, 1956."},{"key":"122366_CR21","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0097-3165(71)90030-6","volume":"10","author":"C. Treash","year":"1971","unstructured":"Treash, Ch.: The completion of finite incomplete Steiner triple systems with applications to loop theory, J. Combinatorial Theory\n10 (1971), 259\u2013265.","journal-title":"J. Combinatorial Theory"},{"key":"122366_CR22","doi-asserted-by":"crossref","unstructured":"Wojcicki, R.: Theory of Logical Calculi: Basic Theory of Consequence Operations, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-94-015-6942-2"},{"key":"122366_CR23","first-page":"305","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\n22 (1984), 305\u2013356.","journal-title":"Artificial Intelligence"},{"key":"122366_CR24","unstructured":"Wos, L., Overbeek, R., Lusk, E. and Boyle, J.: Automated reasoning: Introduction and Applications, 2nd ed., McGraw-Hill, 1992."},{"key":"122366_CR25","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 (1995), 279\u2013315.","journal-title":"J. Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005731217123.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005731217123\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005731217123.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:46:41Z","timestamp":1749124001000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005731217123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,6]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,6]]}},"alternative-id":["122366"],"URL":"https:\/\/doi.org\/10.1023\/a:1005731217123","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,6]]}}}