{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:01Z","timestamp":1747592461566},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544876"},{"type":"electronic","value":"9783540384014"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54487-9_56","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:54:45Z","timestamp":1330210485000},"page":"128-144","source":"Crossref","is-referenced-by-count":2,"title":["A resolution variant deciding some classes of clause sets"],"prefix":"10.1007","author":[{"given":"Christian","family":"Ferm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"8_CR1","volume-title":"The Decision Problem","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., and Goldfarb, W.D., The Decision Problem. Addison-Wesley, Massachusetts 1979."},{"key":"8_CR2","unstructured":"Ferm\u00fcller, C., Deciding some Horn Clause Sets by Resolution. Yearbook of the Kurt G\u00f6del Society 1989, pp. 60\u201373."},{"issue":"1","key":"8_CR3","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"Joyner, W.H., Resolution Strategies as Decision Procedures. J. ACM 23,1 (July 1976), pp. 398\u2013417.","journal-title":"J. ACM"},{"key":"8_CR4","first-page":"87","volume-title":"Machine Intelligence 4","author":"R. Kowalski","year":"1969","unstructured":"Kowalski, R., and Hayes P.J., Semantic trees in automated theorem proving in Machine Intelligence 4, B. Meltzer and D. Michie, Eds., Edinburgh U. Press, Edinburgh 1969, pp. 87\u2013101."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Leitsch, A., Deciding Horn Classes by Hyperresolution. Proc. of the CSL '89, LNCS 440, pp. 225\u2013241.","DOI":"10.1007\/3-540-52753-2_42"},{"key":"8_CR6","volume-title":"Unsolvable Classes of Quantificational Formulas","author":"H.R. Lewis","year":"1979","unstructured":"Lewis, H.R., Unsolvable Classes of Quantificational Formulas. Addison-Wesley, Massachusetts 1979."},{"key":"8_CR7","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"Loveland, D., Automated Theorem Proving: A Logical Basis. North Holland, Amsterdam 1978."},{"key":"8_CR8","first-page":"1420","volume":"5","author":"S. J. Maslov","year":"1964","unstructured":"Maslov, S. Ju., An Inverse Method of Establishing Deducability in the Classical Predicate Calculus. Soviet Math.-Doklady 5 (1964), pp. 1420\u20131424 (translated).","journal-title":"Soviet Math.-Doklady"},{"key":"8_CR9","unstructured":"Maslov, S.Ju., Proof-search Strategies for Methods of the Resolution Type. Machine Intelligence 6, American Elsevier, 1971, pp. 77\u201390."},{"key":"8_CR10","volume-title":"Problem-Solving Methods in Artificial Intelligence","author":"N.J. Nilson","year":"1971","unstructured":"Nilson, N.J., Problem-Solving Methods in Artificial Intelligence. McGraw-Hill, New York, 1971."},{"issue":"1","key":"8_CR11","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A., A Machine-oriented Logic Based on the Resolution Principle. J. ACM 12,1 (Jan. 1965), pp. 23\u201341.","journal-title":"J. ACM"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Tammet, T., A Resolution Program, Able to Decide some Solvable Classes. Proc. of the COLOG '88, LNCS 417, pp. 300\u2013311.","DOI":"10.1007\/3-540-52335-9_61"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0168-0072(89)90053-5","volume":"42","author":"N.K. Zamov","year":"1989","unstructured":"Zamov, N.K., Maslov's Inverse Method and Decidable Classes. Annals of Pure and Applied Logic 42 (1989), pp. 165\u2013194.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54487-9_56.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:55:04Z","timestamp":1605646504000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54487-9_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544876","9783540384014"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-54487-9_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}