{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:39Z","timestamp":1725663879035},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540545637"},{"type":"electronic","value":"9783540384663"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54563-8_121","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T23:03:42Z","timestamp":1330211022000},"page":"580-588","source":"Crossref","is-referenced-by-count":2,"title":["How well are non-horn clauses handled?"],"prefix":"10.1007","author":[{"given":"Xumin","family":"Nie","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"issue":"3","key":"58_CR1","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aaspvall","year":"1979","unstructured":"Aaspvall, B., M.F. Plass and R.E. Tarjan, \u201cA Linear-time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas\u201d, Information Processing Letters 8(3): 121\u2013123, 1979.","journal-title":"Information Processing Letters"},{"doi-asserted-by":"crossref","unstructured":"Cook, S.A. \u201cThe Complexity of Theorem-proving Procedures\u201d, Third Annual ACM Symp. on Theory of Computing, pp. 151\u2013158, 1971.","key":"58_CR2","DOI":"10.1145\/800157.805047"},{"unstructured":"Graham, R.L., D.E. Knuth and O. Patashnik, Concrete Mathematics, Addison-Wesley, 1989.","key":"58_CR3"},{"key":"58_CR4","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"Korf, R.E., \u201cDepth-first Iterative Deepening: an Optimal Admissible Tree Search\u201d, Artificial Intelligence 27: 97\u2013109, 1985.","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Lloyd, J.W., Foundations of Logic Programming, Springer-Verlag, 1987.","key":"58_CR5","DOI":"10.1007\/978-3-642-83189-8"},{"issue":"3","key":"58_CR6","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. W. Loveland","year":"1969","unstructured":"Loveland, D.W., \u201cA Simplified Format for the Model Elimination Theorem-Proving Procedure\u201d, Journal of ACM 16(3): 349\u2013363, 1969.","journal-title":"Journal of ACM"},{"key":"58_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00249353","volume":"7","author":"D. W. Loveland","year":"1991","unstructured":"Loveland, D.W., \u201cNear-Horn Prolog and Beyond\u201d, Journal of Automated Reasoning 7: 1\u201326, 1991.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"Nie, X., \u201cComplexities of Non-Horn Clause Logic Programming\u201d, 5th International Symposium on Methodologies for Intelligent Systems, October, 1990, Knoxville, Tennessee.","key":"58_CR8"},{"key":"58_CR9","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00244355","volume":"6","author":"D. A. Plaisted","year":"1990","unstructured":"Plaisted, D.A., \u201cA Sequent Style Model Elimination Strategy and a Positive Refinement\u201d, Journal of Automated Reasoning 6: 389\u2013402, 1990.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"Stickel, M.E. and M.W. Tyson, \u201cAn Analysis of Consecutively Bounded Depth-first Search with Application in Automated Deduction\u201d, Proc. of IJCAI, pp. 1073\u20131075, 1985.","key":"58_CR10"},{"key":"58_CR11","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M.E., \u201cA PROLOG Technology Theorem Prover\u201d, Journal of Automated Reasoning 4: 353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Methodologies for Intelligent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54563-8_121.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:22:59Z","timestamp":1619572979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54563-8_121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540545637","9783540384663"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-54563-8_121","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}