{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T20:44:33Z","timestamp":1764276273385},"reference-count":47,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1992,10,1]],"date-time":"1992-10-01T00:00:00Z","timestamp":717897600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7594,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1992,10]]},"DOI":"10.1016\/0304-3975(92)90168-f","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"109-128","source":"Crossref","is-referenced-by-count":36,"title":["A Prolog technology theorem prover: a new exposition and implementation in Prolog"],"prefix":"10.1016","volume":"104","author":[{"given":"Mark E.","family":"Stickel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(92)90168-F_BIB1","first-page":"916","article-title":"Terminator","author":"Antoniou","year":"1983","journal-title":"Proc. 8th Internat. Joint Conf. on Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB2","series-title":"Masters Thesis","article-title":"METEOR: model elimination theorem proving for efficient OR-parallelism","author":"Astrachan","year":"1989"},{"key":"10.1016\/0304-3975(92)90168-F_BIB3","article-title":"Parthenon: a parallel theorem prover for non-Horn clauses","author":"Bose","year":"1989","journal-title":"Proc. 4th IEEE Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(92)90168-F_BIB4","first-page":"395","article-title":"Logic programming with general clauses and defaults based on model elimination","author":"Casanova","year":"1989","journal-title":"Proc. 11th Internat. Joint Conf. on Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB5","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/0304-3975(92)90168-F_BIB6","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1007\/3-540-16780-3_125","article-title":"Causes for events: their computation and applications","author":"Cox","year":"1986","journal-title":"Proc. 8th Conf. on Automated Deduction"},{"key":"10.1016\/0304-3975(92)90168-F_BIB7","first-page":"183","article-title":"General diagnosis by abductive inference","author":"Cox","year":"1987","journal-title":"Proc. 1987 Symp. on Logic Programming"},{"key":"10.1016\/0304-3975(92)90168-F_BIB8","series-title":"Ph.D. dissertation","article-title":"Exploiting constraints in design synthesis","author":"Finger","year":"1987"},{"key":"10.1016\/0304-3975(92)90168-F_BIB9","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1145\/321796.321807","article-title":"An implementation of the model elimination proof procedure","volume":"21","author":"Fleisig","year":"1974","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(92)90168-F_BIB10","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0004-3702(72)90045-8","article-title":"The technology chess program","volume":"3","author":"Gillogly","year":"1972","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB11","series-title":"Technical Report 499","article-title":"Interpretation as abduction","author":"Hobbs","year":"1990"},{"key":"10.1016\/0304-3975(92)90168-F_BIB12","series-title":"Technical Report TR-547","article-title":"Procedural interpretation for an extended ATMS","author":"Inoue","year":"1990"},{"key":"10.1016\/0304-3975(92)90168-F_BIB13","article-title":"Consequence-finding based on ordered linear resolution","author":"Inoue","year":"1991","journal-title":"Proc. 12th Internat. Joint Conf. on Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB14","first-page":"212","article-title":"On theorem provers for circumscription","author":"Inoue","year":"1990","journal-title":"Proc. 8th Biennial Conf. of the Canadian Society for Computational Studies of Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","article-title":"Depth-first iterative-deepening: an optimal admissible tree search","volume":"27","author":"Korf","year":"1985","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB16","first-page":"1034","article-title":"Iterative-deepening A\u2217: an optimal admissable tree search","author":"Korf","year":"1985","journal-title":"Proc. 8th Internat. Joint Conf. on Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB17","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":"Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB18","doi-asserted-by":"crossref","unstructured":"R. Letz, J. Schumann, S. Bayerl and W. Bibel, SETHEO: a high-performance theorem prover,J. Automated Reasoning, to appear.","DOI":"10.1007\/BF00244282"},{"key":"10.1016\/0304-3975(92)90168-F_BIB19","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","article-title":"A simplified format for the model elimination procedure","volume":"16","author":"Loveland","year":"1969","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(92)90168-F_BIB20","series-title":"Automated Theorem Proving: A Logical Basis","author":"Loveland","year":"1978"},{"key":"10.1016\/0304-3975(92)90168-F_BIB21","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/BF03037208","article-title":"The Aurora or-parallel Prolog system","volume":"7","author":"Lusk","year":"1990","journal-title":"New Generation Comput."},{"key":"10.1016\/0304-3975(92)90168-F_BIB22","series-title":"Computing with Logic","author":"Maier","year":"1988"},{"key":"10.1016\/0304-3975(92)90168-F_BIB23","series-title":"Ph.D. Dissertation","article-title":"Nonclausal logic programming","author":"Malachi","year":"1986"},{"key":"10.1016\/0304-3975(92)90168-F_BIB24","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0004-3702(72)90047-1","article-title":"A note on linear resolution strategies in consequence finding","volume":"3","author":"Minicozzi","year":"1972","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB25","first-page":"2","article-title":"Model elimination and its positive refinement","volume":"15","author":"Nie","year":"1990","journal-title":"AAR Newsletter"},{"key":"10.1016\/0304-3975(92)90168-F_BIB26","series-title":"DAI Working Paper No. 142","article-title":"Programming meta-logical operations in Prolog","author":"O'Keefe","year":"1983"},{"key":"10.1016\/0304-3975(92)90168-F_BIB27","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","article-title":"Non-Horn clause logic programming without contrapositives","volume":"4","author":"Plaisted","year":"1988","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/0304-3975(92)90168-F_BIB28","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00244355","article-title":"A sequent-style model elimination strategy and a positive refinement","volume":"6","author":"Plaisted","year":"1990","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/0304-3975(92)90168-F_BIB29","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0004-3702(88)90077-X","article-title":"A logical framework for default reasoning","volume":"36","author":"Poole","year":"1988","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB30","first-page":"147","article-title":"On the mechanization of abductive logic","author":"Pople","year":"1973","journal-title":"Proc. 3rd Internat. Joint Conf. on Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB31","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0004-3702(89)90067-2","article-title":"On algorithm to compute circumscription","volume":"38","author":"Przymusininski","year":"1989","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB32","series-title":"Expert Thinker software package","author":"Satz","year":"1988"},{"key":"10.1016\/0304-3975(92)90168-F_BIB33","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/3-540-52885-7_78","article-title":"PARTHEO: a high-performance parallel theorem prover","author":"Schumann","year":"1990","journal-title":"Proc. 10th Internat. Conf. on Automated Deduction"},{"key":"10.1016\/0304-3975(92)90168-F_BIB34","series-title":"Th\u00e8se d'Etat","article-title":"Repr\u00e9sentation et utilisation de la connaissance en calcul propositionnel","author":"Siegel","year":"1987"},{"key":"10.1016\/0304-3975(92)90168-F_BIB35","article-title":"Avoiding duplicate explanations","author":"Spencer","year":"1990","journal-title":"Proc. North-American Conf. on Logic Programming"},{"key":"10.1016\/0304-3975(92)90168-F_BIB36","series-title":"The Art of Prolog","author":"Sterling","year":"1986"},{"key":"10.1016\/0304-3975(92)90168-F_BIB37","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","article-title":"A Prolog technology theorem prover","volume":"2","author":"Stickel","year":"1984","journal-title":"New Generation Computing"},{"key":"10.1016\/0304-3975(92)90168-F_BIB38","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","article-title":"Automated deduction by theory resolution","volume":"1","author":"Stickel","year":"1985","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/0304-3975(92)90168-F_BIB39","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":"4","author":"Stickel","year":"1988","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/0304-3975(92)90168-F_BIB40","series-title":"Technical Note 464","article-title":"A Prolog technology theorem prover: a new exposition and implementation in Prolog","author":"Stickel","year":"1989"},{"key":"10.1016\/0304-3975(92)90168-F_BIB41","doi-asserted-by":"crossref","unstructured":"M.E. Stickel, A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation, Ann. Math. Artificial Intelligence, to appear.","DOI":"10.1007\/BF01531174"},{"key":"10.1016\/0304-3975(92)90168-F_BIB42","article-title":"Rationale and methods for abductive reasoning in natural-language interpretation","author":"Stickel","year":"1989","journal-title":"Proc. IBM Symp. on Natural Language and Logic"},{"key":"10.1016\/0304-3975(92)90168-F_BIB43","first-page":"1073","article-title":"An analysis of consecutively bounded depth-first search with applications in automated deduction","author":"Stickel","year":"1985","journal-title":"Proc. 9th Internat. Joint Conf. on Artificial Intelligence"},{"key":"10.1016\/0304-3975(92)90168-F_BIB44","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/3-540-52885-7_97","article-title":"An examination of the Prolog technology theorem prover","author":"Tarver","year":"1990","journal-title":"Proc. 10th Internat. Conf. on Automated Deduction"},{"key":"10.1016\/0304-3975(92)90168-F_BIB45","first-page":"40","article-title":"An experiment in programming with full first-order logic","author":"Umrigar","year":"1985","journal-title":"Proc. 1985 Symp. on Logic Programming"},{"key":"10.1016\/0304-3975(92)90168-F_BIB46","series-title":"M.Sc. Thesis","article-title":"QUEST: a non-clausal theorem proving system","author":"Wilkins","year":"1973"},{"key":"10.1016\/0304-3975(92)90168-F_BIB47","first-page":"316","article-title":"The linked inference principle, II: the user's viewpoint","author":"Wos","year":"1984","journal-title":"Proc. 7th Internat. Conf. on Automated Deduction"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759290168F?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759290168F?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T04:20:23Z","timestamp":1555129223000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759290168F"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,10]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,10]]}},"alternative-id":["030439759290168F"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(92)90168-f","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1992,10]]}}}