{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:34Z","timestamp":1749124054750},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[1995,6,1]],"date-time":"1995-06-01T00:00:00Z","timestamp":801964800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1995,6]]},"DOI":"10.1007\/bf01530821","type":"journal-article","created":{"date-parts":[[2005,4,18]],"date-time":"2005-04-18T20:41:27Z","timestamp":1113856887000},"page":"225-249","source":"Crossref","is-referenced-by-count":4,"title":["Near-Horn Prolog and the ancestry family of procedures"],"prefix":"10.1007","volume":"14","author":[{"given":"David W.","family":"Reed","sequence":"first","affiliation":[]},{"given":"Donald W.","family":"Loveland","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"O.L. Astrachan","year":"1991","unstructured":"O.L. Astrachan and D.W. Loveland, METEORs: High performance theorem provers for Model Elimination, in:Automated Reasoning: Essays in Honor of Woody Bledsoe, ed. R.S. Boyer (Kluwer, Dordrecht, 1991)."},{"key":"CR2","unstructured":"R. Caferra, E. Eder, B. Fronh\u00f6fer and W. Bibel, Extension of Prolog through matrix reduction,6th European Conf. on Artificial Intelligence, Pisa, Italy (1984)."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1145\/321796.321807","volume":"21","author":"S. Fleisig","year":"1974","unstructured":"S. Fleisig, D. Loveland, A. Smiley and D. Yarmash, An implementation of the Model Elimination proof procedure, J. ACM 21(1974)124?139.","journal-title":"J. ACM"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","volume":"4","author":"D.M. Gabbay","year":"1985","unstructured":"D.M. Gabbay, N-Prolog: An extension of Prolog with hypothetical implication, Part 2, J. Logic Program. 4(1985)251?283.","journal-title":"J. Logic Program."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0743-1066(84)90029-3","volume":"4","author":"D.M. Gabbay","year":"1984","unstructured":"D.M. Gabbay and U. Reyle, N-Prolog: An extension of Prolog with hypothetical implication, Part 1, J. Logic Program. 4(1984)319?355.","journal-title":"J. Logic Program."},{"key":"CR6","unstructured":"R. Hill, LUSH resolution and its completeness, Technical Report DCL Memo 78, Department of Artificial Intelligence, University of Edinburgh (1974)."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R. Kowalski","year":"1971","unstructured":"R. Kowalski and D. Kuehner, Linear resolution with selection function, Artificial Intelligence 2(1971)227?260.","journal-title":"Artificial Intelligence"},{"key":"CR8","unstructured":"R. Kowalski, Predicate calculus as a programming language,Proc. 6th IFIP Congress (North-Holland, 1974) pp. 569?574."},{"key":"CR9","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, S. Bayerl, J. Schumann and W. Bibel, SETHEO ? a high-performance theorm prover, J. Autom. Reasoning 8(1992)183?212.","journal-title":"J. Autom. Reasoning"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"D.W. Loveland, Mechanical theorem proving by model elimination, J. ACM 15(1968)236?251.","journal-title":"J. ACM"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D.W. Loveland","year":"1969","unstructured":"D.W. Loveland, A simplified format for the Model Elimination procedure, J. ACM 16(1969)349?363.","journal-title":"J. ACM"},{"key":"CR12","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":"CR13","doi-asserted-by":"crossref","unstructured":"D.W. Loveland, Near-Horn Prolog, in:Logic Programming: Proc. 4th Int. Conf., ed. J. Lassez (MIT Press, 1987) pp. 456?469.","DOI":"10.21236\/ADA185172"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00249353","volume":"7","author":"D.W. Loveland","year":"1991","unstructured":"D.W. Loveland, Near-Horn Prolog and beyond, J. Autom. Reasoning 7(1991)1?26.","journal-title":"J. Autom. Reasoning"},{"key":"CR15","unstructured":"D.W. Loveland and D.W. Reed, A near-Horn Prolog for compilation, in:Computational Logic: Essays in Honor of Alan Robinso, ed. J. Lassez (MIT Press, 1991)."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0020-0190(82)90035-7","volume":"14","author":"J. Minker","year":"1982","unstructured":"J. Minker and G. Zanon, An extension to linear resolution with selection function, Inf. Proces. Lett. 14(1982)191?194.","journal-title":"Inf. Proces. Lett."},{"key":"CR17","unstructured":"L.M. Pereira, L. Caires and J. Alferes, Classical negation for normal logic programs,Proc. 7th ?Semin\u00e1rio Brasileiro de Intelig\u00eancia Artificial?, (1990)."},{"key":"CR18","first-page":"1","volume-title":"Lecture Notes in Artificial Intelligence 660","author":"L.M. Pereira","year":"1993","unstructured":"L.M. Pereira, L. Caires and J. Alferes, SLWV ? a theorem prover for logic programming,Proc. 3rd Workshop on Extensions of Logic Programming (ELP '92), Lecture Notes in Artificial Intelligence 660 (Springer, Berlin, 1993) pp. 1?23."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","volume":"18","author":"D. Plaisted","year":"1982","unstructured":"D. Plaisted, A simplified problem reduction format, Artificial Intelligence 18(1982)227?261.","journal-title":"Artificial Intelligence"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"D. Plaisted, Non-Horn clause logic programming without contrapositives, J. Autom. Reasoning 4(1988)287?325.","journal-title":"J. Autom. Reasoning"},{"key":"CR21","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00244355","volume":"6","author":"D. Plaisted","year":"1990","unstructured":"D. Plaisted, A sequent style Model Elimination strategy and a positive refinement, J. Autom. Reasoning 6(1990)389?402.","journal-title":"J. Autom. Reasoning"},{"key":"CR22","unstructured":"D.W. Reed, A case-analysis approach to disjunctive logic programming, Ph.D. Thesis, Duke University (1992)."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"D.W. Reed and D.W. Loveland, A comparison of three Prolog extensions, J. Logic Program. 12(1) (1992).","DOI":"10.1016\/0743-1066(92)90038-5"},{"key":"CR24","first-page":"345","volume-title":"Lecture Notes in Artificial Intelligence 596","author":"D.W. Reed","year":"1992","unstructured":"D.W. Reed, D.W. Loveland and B.T. Smith, A near-Horn approach to disjunctive logic programming,Proc. 2nd Workshop on Extensions of Logic Programming (ELP '91), Lecture Notes in Artificial Intelligence 596 (Springer, Berlin, 1992) pp. 345?369."},{"key":"CR25","unstructured":"M.E. Stickel and D.W. Loveland, A hole in goal trees: Some guidance from Resolution theory,Proc. 3rd Int. Joint Conf. on Artificial Intelligence (1973) pp. 153?161. Also in IEEE Trans. Comp. C-25 (April 1976)."},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"J. Schumann and R. Letz, PARTHEO ? a high performance parallel theorem prover,Proc. 10th Int. Conf. on Automated Deduction (1990) pp. 40?56.","DOI":"10.1007\/3-540-52885-7_78"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","volume":"2","author":"M.E. Stickel","year":"1984","unstructured":"M.E. Stickel, A Prolog technology theorem prover, New Generation Comp. 2(1984)371?383.","journal-title":"New Generation Comp."},{"key":"CR28","unstructured":"T. Wakayama, Indefinite query answers in deductive knowledge bases,Proc. 3rd IASTED Int. Symp. on Expert Systems Theory and Applications (1988)."},{"key":"CR29","unstructured":"T. Wakayama, Reasoning with indefinite information in Resolution-based languages, Ph.D. Thesis, Syracuse University (1989)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01530821\/fulltext.html","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01530821.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01530821\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01530821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T09:31:30Z","timestamp":1556875890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01530821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,6]]},"references-count":29,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[1995,6]]}},"alternative-id":["BF01530821"],"URL":"https:\/\/doi.org\/10.1007\/bf01530821","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,6]]}}}