{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:09:57Z","timestamp":1754482197986},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600176"},{"type":"electronic","value":"9783540494041"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022263","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T01:12:29Z","timestamp":1132621949000},"page":"279-293","source":"Crossref","is-referenced-by-count":8,"title":["Resolution games and non-liftable resolution orderings"],"prefix":"10.1007","author":[{"given":"Hans","family":"de Nivelle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"21_CR1","volume-title":"LPAR92","author":"P. Baumgartner","year":"1992","unstructured":"P. Baumgartner, An ordered theory calculus, in LPAR92, Springer Verlag, Berlin, 1992."},{"key":"21_CR2","first-page":"427","volume-title":"CADE 10","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair, H. Ganzinger, On restrictions of ordered paramodulation with simplification, CADE 10, pp 427\u2013441, Keiserslautern, Germany, Springer Verlag, 1990."},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0304-3975(90)90139-9","volume":"74","author":"M. Bezem","year":"1990","unstructured":"M. Bezem, Completeness of resolution revisited, Theoretical computer science 74, pp. 227\u2013237, 1990.","journal-title":"Theoretical computer science"},{"key":"21_CR4","volume-title":"Ph. D. Thesis","author":"R.S. Boyer","year":"1971","unstructured":"R.S. Boyer, Locking: A restriction of resolution, Ph. D. Thesis, University of Texas at Austin, Texas 1971."},{"key":"21_CR5","volume-title":"Symbolic logic and mechanical theorem proving","author":"C-L. Chang","year":"1973","unstructured":"C-L. Chang, R.C-T. Lee, Symbolic logic and mechanical theorem proving, Academic Press, New York 1973."},{"doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, N. Zamov, Resolution methods for the decision problem, Springer Verlag, 1993.","key":"21_CR6","DOI":"10.1007\/3-540-56732-1"},{"issue":"1","key":"21_CR7","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"W.H. Joyner, Resolution Strategies as Decision Procedures, J. ACM 23, 1 (July 1976), pp. 398\u2013417.","journal-title":"J. ACM"},{"key":"21_CR8","volume-title":"Machine Intelligence 4","author":"R. Kowalski","year":"1969","unstructured":"R. Kowalski, P.J. Hayes, Semantic trees in automated theorem proving, Machine Intelligence 4, B. Meltzer and D. Michie, Edingburgh University Press, Edingburgh, 1969."},{"unstructured":"H. de Nivelle, Resolution games and non-liftable resolution orderings, Internal report 94-36, Department of Mathematics and Computer Science, Delft University of Technology.","key":"21_CR9"},{"key":"21_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson, A machine oriented logic based on the resolution principle, Journal of the ACM, Vol. 12, pp 23\u201341, 1965.","journal-title":"Journal of the ACM"},{"unstructured":"T. Tammet, Seperate orderings for ground and non-ground literals preserve completeness of resolution, unpublished, 1994.","key":"21_CR11"},{"key":"21_CR12","first-page":"5","volume":"128","author":"N.K. Zamov","year":"1972","unstructured":"N.K. Zamov: On a Bound for the Complexity of Terms in the Resolution Method, Trudy Mat. Inst. Steklov 128, pp. 5\u201313, 1972.","journal-title":"Trudy Mat. Inst. Steklov"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022263","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T17:12:01Z","timestamp":1554570721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022263"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0022263","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}