{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:41:59Z","timestamp":1747546919447},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"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":[[1996,9]]},"DOI":"10.1007\/bf02127749","type":"journal-article","created":{"date-parts":[[2005,9,15]],"date-time":"2005-09-15T07:34:26Z","timestamp":1126769666000},"page":"243-260","source":"Crossref","is-referenced-by-count":3,"title":["On resolution with short clauses"],"prefix":"10.1007","volume":"18","author":[{"given":"Michael","family":"Buro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans Kleine","family":"B\u00fcning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02127749_CR1","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and I.H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulas,I. Logic Programming 3 (1984) 267\u2013284.","journal-title":"I. Logic Programming"},{"key":"BF02127749_CR2","doi-asserted-by":"crossref","unstructured":"E. Eder,Relative Complexities of First Order Calculi (Vieweg, 1992).","DOI":"10.1007\/978-3-322-84222-0"},{"key":"BF02127749_CR3","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0020-0190(88)90113-5","volume":"29","author":"G. Gallo","year":"1988","unstructured":"G. Gallo and M.G. Scutell\u00e0, Polynomially satisfiability problems,Information Processing Letters 29 (1988) 267\u2013284.","journal-title":"Information Processing Letters"},{"key":"BF02127749_CR4","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken, The intractability of resolution,TCS 39 (1985) 297\u2013308.","journal-title":"TCS"},{"key":"BF02127749_CR5","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1016\/0304-3975(93)90331-M","volume":"116","author":"H. Kleine B\u00fcning","year":"1993","unstructured":"H. Kleine B\u00fcning, On generalized Horn formulas andk-resolution,TCS 116 (1993) 405\u2013413.","journal-title":"TCS"},{"key":"BF02127749_CR6","unstructured":"G.S. Tseitin, On the complexity of derivations in the propositional calculus, in:Structures in Constructive Mathematics and Mathematical Logic, Part II, ed. A.O. Slisenko (1968) pp. 115\u2013125."},{"key":"BF02127749_CR7","doi-asserted-by":"crossref","unstructured":"L. Wos, D. Carson and G.A. Robinson, The unit preference strategy in theorem proving,AFIPS Conf. Proc. 26 (Spantau Books, Washington, DC).","DOI":"10.1145\/1464052.1464109"},{"key":"BF02127749_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(83)80027-8","volume":"59","author":"S. Yamasaki","year":"1983","unstructured":"S. Yamasaki and S. Doshita, The satisfiability problem for a class consisting of Horn sentences and some none-Horn sentences in propositional logic,Information and Control 59 (1983) 1\u201312.","journal-title":"Information and Control"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127749.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02127749\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127749","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T21:45:38Z","timestamp":1557783938000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02127749"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":8,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["BF02127749"],"URL":"https:\/\/doi.org\/10.1007\/bf02127749","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}