{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T04:01:17Z","timestamp":1747627277293,"version":"3.40.5"},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1998,11,1]],"date-time":"1998-11-01T00:00:00Z","timestamp":909878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,11,1]],"date-time":"1998-11-01T00:00:00Z","timestamp":909878400000},"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":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[1998,11]]},"DOI":"10.1023\/a:1018976510663","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"247-266","source":"Crossref","is-referenced-by-count":3,"title":["Heuristics used by HERBY for semantic tree theorem proving"],"prefix":"10.1007","volume":"23","author":[{"given":"Qingxun","family":"Yu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohammed","family":"Almulla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Monroe","family":"Newborn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"325499_CR1","volume-title":"Analysis of the use of semantic trees in automated theorem proving","author":"M. Almulla","year":"1995","unstructured":"M. Almulla, Analysis of the use of semantic trees in automated theorem proving, Ph.D. thesis, School of Computer Science, McGill University, Montreal, Canada (1995)."},{"key":"325499_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.L. Chang","year":"1973","unstructured":"C.L. Chang and R.C.T. Lee, Symbolic Logic and Mechanical Theorem Proving(Academic Press, New York, 1973)."},{"key":"325499_CR3","volume-title":"Theorem Proving by Generation of Pseudo-Semantic Trees","author":"C.L. Chang","year":"1971","unstructured":"C.L. Chang, Theorem Proving by Generation of Pseudo-Semantic Trees(Division of Computer Research and Technology, NIT, Bethesda, MD, 1971)."},{"issue":"3","key":"325499_CR4","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of ACM 38(3) (1991) 559\u2013587.","journal-title":"Journal of ACM"},{"key":"325499_CR5","first-page":"87","volume":"4","author":"R. Kowalski","year":"1969","unstructured":"R. Kowalski and J.P. Hayes, Semantic trees in automatic theorem proving, Machine Intelligence 4 (1969) 87\u2013101.","journal-title":"Machine Intelligence"},{"issue":"2","key":"325499_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, S. Bayerl and W. Bibel, SETHEO, a high performance theorem prover, Journal of Automated Reasoning 8(2) (1992) 183\u2013213.","journal-title":"Journal of Automated Reasoning"},{"key":"325499_CR7","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D.W. Loveland","year":"1978","unstructured":"D.W. Loveland, Automated Theorem Proving: A Logical Basis(North-Holland, Amsterdam, 1978)."},{"key":"325499_CR8","unstructured":"Z. Manna, Mathematical Theory of Computation, Computer Science Series (McGraw-Hill, 1974)."},{"key":"325499_CR9","volume-title":"The Great Theorem Prover, Version 2","author":"M. Newborn","year":"1994","unstructured":"M. Newborn, The Great Theorem Prover, Version 2(Newborn Software, Montreal, 1994)."},{"key":"325499_CR10","volume-title":"Logical Foundations of Artificial Intelligence","author":"N.J. Nilsson","year":"1987","unstructured":"N.J. Nilsson and M.R. Genesereth, Logical Foundations of Artificial Intelligence(Morgan Kaufmann, San Mateo, CA, 1987)."},{"issue":"1","key":"325499_CR11","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"J. Robinson, A machine-oriented logic based on the resolution principle, Journal of ACM 12(1) (1965) 601\u2013607.","journal-title":"Journal of ACM"},{"issue":"4","key":"325499_CR12","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J.R. Slagle","year":"1967","unstructured":"J.R. Slagle, Automatic theorem-proving with renameable and semantic resolution, Journal of ACM 14(4) (1967) 687\u2013697.","journal-title":"Journal of ACM"},{"issue":"4","key":"325499_CR13","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M.E. Stickel","year":"1988","unstructured":"M.E. Stickel, A Prolog technology theorem prover: implementation by an extended Prolog compiler, Journal of Automated Reasoning 4(4) (1988) 353\u2013380.","journal-title":"Journal of Automated Reasoning"},{"key":"325499_CR14","volume-title":"Set Theory and Logic","author":"R. Stoll","year":"1963","unstructured":"R. Stoll, Set Theory and Logic(W.H. Freeman, New York, 1963)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018976510663.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018976510663\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018976510663.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:46:17Z","timestamp":1747547177000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018976510663"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,11]]},"references-count":14,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1998,11]]}},"alternative-id":["325499"],"URL":"https:\/\/doi.org\/10.1023\/a:1018976510663","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[1998,11]]}}}