{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:40:00Z","timestamp":1749123600879,"version":"3.41.0"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"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,12]]},"DOI":"10.1023\/a:1006027228476","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:38:24Z","timestamp":1040517504000},"page":"381-400","source":"Crossref","is-referenced-by-count":1,"title":["Well-Behaved Inference Rules for First-Order Theorem Proving"],"prefix":"10.1007","volume":"21","author":[{"given":"Jinzhao","family":"Wu","sequence":"first","affiliation":[]},{"given":"Zhuojun","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"181211_CR1","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.-L. Chang","year":"1973","unstructured":"Chang, C.-L. and Lee, R. C.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"181211_CR2","volume-title":"Topics in automated theorem proving and program generation","author":"J. Hsiang","year":"1982","unstructured":"Hsiang, J.: Topics in automated theorem proving and program generation, Ph.D. Thesis, University of Illinois at Urbana-Champaign, UIUCDCS-R-82-1113, 1982."},{"key":"181211_CR3","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"Hsiang, J.: Refutational theorem proving using term-rewriting systems, Artif. Intell.\n25 (1985), 255\u2013300.","journal-title":"Artif. Intell."},{"key":"181211_CR4","doi-asserted-by":"crossref","unstructured":"Kapur, D., and Narendran, P.: An Equational Approach to Theorem Proving in First-Order Predicate Calculus, 84CRD322, GE Research Lab., 1985.","DOI":"10.1145\/1012497.1012521"},{"key":"181211_CR5","doi-asserted-by":"crossref","unstructured":"Knuth, D. E. and Bendix, P. B.: Simple word problems in universal algebras, in J. Leech (ed.), Computational Problems in Abstract Algebras, Pergamon Press, 1970, pp. 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"2","key":"181211_CR6","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/BF02939497","volume":"9","author":"X. H. Liu","year":"1994","unstructured":"Liu, X. H. and Sun, J. G.: Generalized resolution and NC-resolution, J. Comput. Sci. and Technol.\n9(2) (1994), 160\u2013167.","journal-title":"J. Comput. Sci. and Technol."},{"key":"181211_CR7","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"Loveland, D.: Automated Theorem Proving: A Logical Basis, North-Holland, New York, 1978."},{"key":"181211_CR8","doi-asserted-by":"crossref","unstructured":"Muller, J. and Socher-Ambrosius, R.: On the unnecessity of multiple overlaps in completion theorem proving, in Proc. 12th GWAI, IFB 181, 1988.","DOI":"10.1007\/978-3-642-74064-0_18"},{"issue":"1","key":"181211_CR9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","volume":"18","author":"N. V. Murray","year":"1982","unstructured":"Murray, N. V.: Completely non-clausal theorem proving, Artif. Intell.\n18(1) (1982), 67\u201385.","journal-title":"Artif. Intell."},{"issue":"2","key":"181211_CR10","first-page":"81","volume":"5","author":"X. H. Wang","year":"1982","unstructured":"Wang, X. H. and Liu, X. H.: Generalized resolution, Chinese J. Computer\n5(2) (1982), 81\u201392.","journal-title":"Chinese J. Computer"},{"key":"181211_CR11","unstructured":"Wu, J. Z. and Liu, Z. J.: Linear strategy, semantic strategy and lock strategy in remainder method, accepted by Chinese J. Computer."},{"key":"181211_CR12","unstructured":"Wu, J. Z. and Liu, Z. J.: The remainder method for the first-order theorem proving, accepted by Chinese J. Computer."},{"key":"181211_CR13","volume-title":"Automated Reasoning: 33 Basic Problems","author":"L. Wos","year":"1988","unstructured":"Wos, L.: Automated Reasoning: 33 Basic Problems, Prentice-Hall, Englewood Cliffs, New Jersey, 1988."},{"key":"181211_CR14","first-page":"207","volume":"4","author":"W. T. Wu","year":"1984","unstructured":"Wu, W. T.: Basic principles of mechanical theorem proving in elementary geometries, J. Systems Sci. Math. Sci.\n4 (1984), 207\u2013235.","journal-title":"J. Systems Sci. Math. Sci."},{"key":"181211_CR15","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1006\/jsco.1994.1011","volume":"17","author":"H. Zhang","year":"1994","unstructured":"Zhang, H.: A new method for the Boolean ring based theorem proving, J. Symbolic Comput.\n17 (1994), 189\u2013211.","journal-title":"J. Symbolic Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006027228476.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006027228476\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006027228476.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:27:24Z","timestamp":1749122844000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006027228476"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,12]]},"references-count":15,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,12]]}},"alternative-id":["181211"],"URL":"https:\/\/doi.org\/10.1023\/a:1006027228476","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,12]]}}}