{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T23:52:48Z","timestamp":1676677968965},"reference-count":40,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1997,5,1]],"date-time":"1997-05-01T00:00:00Z","timestamp":862444800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T00:00:00Z","timestamp":1374710400000},"content-version":"vor","delay-in-days":5929,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1997,5]]},"DOI":"10.1016\/s0004-3702(96)00046-x","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:24:09Z","timestamp":1027643049000},"page":"25-89","source":"Crossref","is-referenced-by-count":7,"title":["Clause trees: a tool for understanding and implementing resolution in automated reasoning"],"prefix":"10.1016","volume":"92","author":[{"given":"J.D.","family":"Horton","sequence":"first","affiliation":[]},{"given":"Bruce","family":"Spencer","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0004-3702(96)00046-X_BIB1","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1109\/TC.1976.1674698","article-title":"Refutations by matings","volume":"25","author":"Andrews","year":"1976","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB2","series-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","article-title":"METEORs: high performance theorem provers using model elimination","author":"Astrachan","year":"1991"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB3","series-title":"Automated Deduction\u2014 CADE-11","first-page":"224","article-title":"Caching and lemmaizing in model elimination theorem provers","volume":"607","author":"Astrachan","year":"1992"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB4","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244489","article-title":"Short proof of the pigeonhole formulas based on the connection method","volume":"6","author":"Bibel","year":"1990","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB5","author":"Chang","year":"1973"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB6","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","article-title":"Many hard examples for resolution","volume":"35","author":"Chv\u00e1tal","year":"1988","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB7","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook","year":"1979","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB8","article-title":"Completeness, Confluence and Related Properties of Clause Graph Resolution","author":"Eisinger","year":"1991"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB9","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB10","author":"Harary","year":"1969"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB11","unstructured":"J.D. Horton and D. Sharpe, private communication."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB12","series-title":"KI-95 Activities: Workshops, Posters, Demos","first-page":"79","article-title":"A top down algorithm to find only minimal clause trees","author":"Horton","year":"1995"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB13","article-title":"Reducing search with minimal clause trees","author":"Horton","year":"1995"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB14","article-title":"Bottom-up procedures for minimal clause trees","author":"Horton","year":"1996"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB15","article-title":"The disequality strategy in theorem proving","author":"Hynes","year":"1995"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB16","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear resolution with selection function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artif. Intell."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB17","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","article-title":"Controlled integration of the cut rule into connection tableau calculi","volume":"13","author":"Letz","year":"1994","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB18","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","article-title":"SETHEO: a high-performance theorem prover","volume":"8","author":"Letz","year":"1992","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB19","author":"Lobo","year":"1992"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB20","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","article-title":"Mechanical theorem proving by model elimination","volume":"15","author":"Loveland","year":"1968","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB21","author":"Loveland","year":"1978"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB22","article-title":"OTTER 2.0 users guide","author":"McCune","year":"1990"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB23","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0020-0190(82)90035-7","article-title":"An extension to linear resolution with selection function","volume":"14","author":"Minker","year":"1982","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB24","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/174130.174135","article-title":"Dissolution: making paths vanish","volume":"40","author":"Murray","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB25","doi-asserted-by":"crossref","first-page":"630","DOI":"10.1145\/321662.321678","article-title":"Two results on ordering for resolution with merging and linear format","volume":"18","author":"Reiter","year":"1971","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB26","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB27","article-title":"AllPaths theorem prover","author":"Sharpe","year":"1995"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB28","series-title":"Proceedings of the Ninth Florida Artificial Intelligence Research Symposium","first-page":"459","article-title":"Backwards basic factoring: a pessimistic analog of basic factoring","author":"Sharpe","year":"1996"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB29","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","article-title":"Refutation graphs","volume":"7","author":"Shostak","year":"1976","journal-title":"Artif. Intell."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB30","series-title":"Proceedings ILPS Workshop\u2014Disjunctive Logic Programming","article-title":"Linear resolution with ordered clauses","author":"Spencer","year":"1991"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB31","series-title":"Proceedings International Symposium of Logic Programming","first-page":"678","article-title":"The ordered clause restriction of model elimination and SLI resolution","author":"Spencer","year":"1993"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB32","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01530763","article-title":"Avoiding duplicate proofs with the foothold refinement","volume":"12","author":"Spencer","year":"1994","journal-title":"Ann. Math. Artif. Intell."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB33","article-title":"Experiments with the ALPOC theorem prover","author":"Spencer","year":"1995"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB34","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","article-title":"A Prolog technology theorem prover: implementation by an extended Prolog compiler","volume":"1","author":"Stickel","year":"1988","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB35","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(92)90168-F","article-title":"A Prolog technology theorem prover: a new exposition and implementation in Prolog","volume":"104","author":"Stickel","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB36","unstructured":"M. Stickel, personal communication."},{"key":"10.1016\/S0004-3702(96)00046-X_BIB37","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF00881955","article-title":"Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction","volume":"13","author":"Stickel","year":"1994","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB38","series-title":"Automated Deduction\u2014CADE-12","first-page":"252","article-title":"The TPTP problem library","volume":"814","author":"Sutcliffe","year":"1994"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB39","series-title":"Studies in Mathematics and Mathematical Logic Part II","first-page":"115","article-title":"On the complexity of derivations in prepositional calculus","author":"Tseitin","year":"1970"},{"key":"10.1016\/S0004-3702(96)00046-X_BIB40","author":"Wos","year":"1988"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S000437029600046X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S000437029600046X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T06:28:37Z","timestamp":1555050517000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S000437029600046X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,5]]},"references-count":40,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1997,5]]}},"alternative-id":["S000437029600046X"],"URL":"https:\/\/doi.org\/10.1016\/s0004-3702(96)00046-x","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1997,5]]}}}