{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T03:59:52Z","timestamp":1648785592935},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2000,9,1]],"date-time":"2000-09-01T00:00:00Z","timestamp":967766400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. & Technol."],"published-print":{"date-parts":[[2000,9]]},"DOI":"10.1007\/bf02950403","type":"journal-article","created":{"date-parts":[[2008,9,13]],"date-time":"2008-09-13T18:02:55Z","timestamp":1221328975000},"page":"409-415","source":"Crossref","is-referenced-by-count":0,"title":["Renaming a set of non-Horn clauses"],"prefix":"10.1007","volume":"15","author":[{"given":"Xumin","family":"Nie","sequence":"first","affiliation":[]},{"given":"Qing","family":"Guo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF02950403_CR1","unstructured":"Clocksin W F, Mellish C S. Programming in Prolog. Springer-Verlag, 1981."},{"key":"BF02950403_CR2","doi-asserted-by":"crossref","unstructured":"Lloyd J W. Foundations of Logic Programming. Springer-Verlag, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"BF02950403_CR3","unstructured":"Kowalski R A. Predicate logic as a programming language. InInformation Processing 74, Jack Rosenfeld (ed.), North-Holland, 1974, pp.569\u2013574."},{"issue":"3","key":"BF02950403_CR4","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881948","volume":"13","author":"P Baumgartner","year":"1994","unstructured":"Baumgartner P, Furbach U. Model elimination without contrapositives and its application to PTTP.Journal of Automated Reasoning, 1994, 13(3): 339\u2013359.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"BF02950403_CR5","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D W Loveland","year":"1969","unstructured":"Loveland D W. A simplified format for the model elimination theorem-proving procedure.Journal of ACM, 1969, 16(3): 349\u2013363.","journal-title":"Journal of ACM"},{"issue":"1","key":"BF02950403_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00249353","volume":"7","author":"D W Loveland","year":"1991","unstructured":"Loveland D W. Near-Horn Prolog and beyond.Journal of Automated Reasoning, 1991, 7(1): 1\u201326.","journal-title":"Journal of Automated Reasoning"},{"key":"BF02950403_CR7","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","volume":"18","author":"D A Plaisted","year":"1982","unstructured":"Plaisted D A. A simplified problem reduction format.Artificial Intelligence, 1982, 18: 227\u2013261.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"BF02950403_CR8","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D A Plaisted","year":"1988","unstructured":"Plaisted D A. Non-Horn clause logic programming without contrapositives.Journal of Automated Reasoning, 1988, 4(3): 287\u2013325.","journal-title":"Journal of Automated Reasoning"},{"key":"BF02950403_CR9","doi-asserted-by":"crossref","unstructured":"Reed D W, Loveland D W. Near-Horn Prolog and the ancestry family of procedures.Annals of Mathematics and Artificial Intelligence, 1995, 14.","DOI":"10.1007\/BF01530821"},{"key":"BF02950403_CR10","unstructured":"Nie X. Complexities of non-Horn clause logic programming. InMethodologies for Intelligent Systems 5, Ras Z, Zemankova M, Emrich M (eds.), 1990, p.539\u2013544."},{"key":"BF02950403_CR11","doi-asserted-by":"crossref","unstructured":"Nie X. How well are non-Horn clauses handled. InLecture Notes in Computer Science 542, Ras Z, Zemankova M (eds.), Springer-Verlag, 1991, pp.580\u2013588.","DOI":"10.1007\/3-540-54563-8_121"},{"key":"BF02950403_CR12","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0004-3702(97)00007-6","volume":"92","author":"X Nie","year":"1997","unstructured":"Nie X. A note on non-Horn clause logic programming.Artificial Intelligence, 1997, 92: 243\u2013258.","journal-title":"Artificial Intelligence"},{"key":"BF02950403_CR13","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0743-1066(92)90038-5","volume":"12","author":"D W Reed","year":"1992","unstructured":"Reed D W, Loveland D W. A comparison of three Prolog extensions.Journal of Logic Programming, 1992, 12: 25\u201350.","journal-title":"Journal of Logic Programming"},{"key":"BF02950403_CR14","unstructured":"Mitchell D, Selman B, Levesque H. Hard and easy distributions of SAT problems. InProceeding of AAAI-92, San Jose, CA, July 12\u201316, 1992, pp.459\u2013465."},{"issue":"1","key":"BF02950403_CR15","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H R Lewis","year":"1978","unstructured":"Lewis H R. Renaming a set of clauses as a Horn set.Journal of ACM, 1978, 25(1): 134\u2013135.","journal-title":"Journal of ACM"},{"issue":"5","key":"BF02950403_CR16","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(85)90096-1","volume":"21","author":"H Mannila","year":"1985","unstructured":"Mannila H, Mehlhorn K. A fast algorithm for renaming a set of clauses as a Horn set.Information Processing Letter, 1985, 21(5): 269\u2013272.","journal-title":"Information Processing Letter"},{"key":"BF02950403_CR17","unstructured":"Garey M R, Johnson D S. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman Company, 1979."},{"issue":"4","key":"BF02950403_CR18","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"L Henschen","year":"1974","unstructured":"Henschen L, Wos L. Unit refutations and Horn sets.Journal of ACM, 1974, 21(4): 590\u2013605.","journal-title":"Journal of ACM"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02950403.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02950403\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02950403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T20:36:04Z","timestamp":1558470964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02950403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,9]]},"references-count":18,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2000,9]]}},"alternative-id":["BF02950403"],"URL":"https:\/\/doi.org\/10.1007\/bf02950403","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,9]]}}}