{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:01Z","timestamp":1749125401318,"version":"3.41.0"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2000,7,1]],"date-time":"2000-07-01T00:00:00Z","timestamp":962409600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,7,1]],"date-time":"2000-07-01T00:00:00Z","timestamp":962409600000},"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":[[2000,7]]},"DOI":"10.1023\/a:1006241826565","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"1-34","source":"Crossref","is-referenced-by-count":2,"title":["Efficient Algorithms to Detect and Restore Minimality, an Extension of the Regular Restriction of Resolution"],"prefix":"10.1007","volume":"25","author":[{"given":"Bruce","family":"Spencer","sequence":"first","affiliation":[]},{"given":"J. D.","family":"Horton","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"211861_CR1","first-page":"1259","volume":"3","author":"G. M. Adelson-Velskii","year":"1962","unstructured":"Adelson-Velskii, G. M. and Landis, E. M.: An algorithm for the organization of information, Soviet Math. Dokl.\n3 (1962), 1259\u20131263.","journal-title":"Soviet Math. Dokl."},{"key":"211861_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, Chin-Liang and Char-Tung Lee, Richard: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"211861_CR3","first-page":"1","volume":"2","author":"d. N. Hans","year":"1996","unstructured":"de Nivelle, Hans: Resolution games and non-liftable resolution orderings, Collegium Logicum, Ann. of the Kurt G\u00f6del Soc.\n2 (1996), 1\u201320.","journal-title":"Collegium Logicum, Ann. of the Kurt G\u00f6del Soc."},{"key":"211861_CR4","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1137\/0222044","volume":"22","author":"G. Andreas","year":"1993","unstructured":"Goerdt, Andreas: Regular resolution versus unrestricted resolution, SIAMJ. Comput.\n22 (1993), 661\u2013683.","journal-title":"SIAMJ. Comput."},{"key":"211861_CR5","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/S0004-3702(96)00046-X","volume":"92","author":"J. D. Horton","year":"1997","unstructured":"Horton, J. D. and Spencer, B.: Clause trees: A tool for understanding and implementing resolution in automated reasoning, Artif. Intell.\n92 (1997), 25\u201389.","journal-title":"Artif. Intell."},{"key":"211861_CR6","series-title":"Lecture Notes in Artif. Intell.","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/BFb0054275","volume-title":"Automated Deduction-CADE-15","author":"J. D. Horton","year":"1998","unstructured":"Horton, J. D. and Spencer, B.: Rank\/activity: A canonical form for binary resolution, in: C. Kirchner and H. Kirchner (eds), Automated Deduction-CADE-15, Lecture Notes in Artif. Intell. 1421, Springer-Verlag, Berlin, July 1998, pp. 412\u2013426."},{"key":"211861_CR7","series-title":"Technical Report TR97-115","volume-title":"Bottom up procedures to construct each minimal clause tree once","author":"J. D. Horton","year":"1997","unstructured":"Horton, J. D. and Spencer, B.: Bottom up procedures to construct each minimal clause tree once, Technical Report TR97-115, Faculty of Computer Science, University of New Brunwsick, PO Box 4400, Fredericton, New Brunswick, Canada, 1997."},{"key":"211861_CR8","first-page":"1","volume":"10","author":"S. Kleene","year":"1952","unstructured":"Kleene, S.: On the permutability of inferences, Memoirs of the AMS\n10 (1952), 1\u201326.","journal-title":"Memoirs of the AMS"},{"key":"211861_CR9","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. Loveland","year":"1968","unstructured":"Loveland, Donald:Mechanical theorem proving by model elimination, J. ACM\n15 (1968), 236\u2013251.","journal-title":"J. ACM"},{"key":"211861_CR10","series-title":"Technical Report ANL-94\/6","volume-title":"Otter 3.0 users guide","author":"W. W. McCune","year":"1994","unstructured":"McCune, W. W.: Otter 3.0 users guide, Technical Report ANL-94\/6, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1994."},{"key":"211861_CR11","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K. and Goller, C.: Controlled integration of the cut rule into connection tableau calculi, J. Automated Reasoning\n13 (1994), 297\u2013337.","journal-title":"J. Automated Reasoning"},{"key":"211861_CR12","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. ACM\n12 (1965), 23\u201341.","journal-title":"J. ACM"},{"key":"211861_CR13","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1145\/3828.3835","volume":"32","author":"D. D. Sleator","year":"1985","unstructured":"Sleator, D. D. and Tarjan, R. E.: Self-adjusting binary search trees, J. ACM\n32 (1985), 652\u2013686.","journal-title":"J. ACM"},{"key":"211861_CR14","unstructured":"Spencer, Bruce and Horton, J. D.: Extending the regular restriction of resolution to non-linear subdeductions, in Proceedings of the Fourteenth National Conference on Artificial Intelligence, AAAI Press\/MIT Press, 1997, pp. 478\u2013483."},{"key":"211861_CR15","doi-asserted-by":"crossref","unstructured":"Tseitin, G. S.: On the complexity of derivation in propositional calculus, in Studies in Constructive Mathematics, Seminars in Mathematics: Matematicheskii Institute, Consultants Bureau, 1969, pp. 115\u2013125.","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006241826565.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006241826565\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006241826565.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:39:23Z","timestamp":1749123563000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006241826565"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,7]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,7]]}},"alternative-id":["211861"],"URL":"https:\/\/doi.org\/10.1023\/a:1006241826565","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2000,7]]}}}