{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:13Z","timestamp":1725456073900},"publisher-location":"Berlin\/Heidelberg","reference-count":13,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354058403X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0016842","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:52:57Z","timestamp":1132714377000},"page":"19-33","source":"Crossref","is-referenced-by-count":0,"title":["Simplifying clausal satisfiability problems"],"prefix":"10.1007","author":[{"given":"Peter","family":"Barth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"P. Barth. Linear 0\u20131 inequalities and extended clauses. In Logic Programming and Automated Reasoning: international conference LPAR '93; St. Petersburg, Russia; proceedings, July 1993.","DOI":"10.1007\/3-540-56944-8_40"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"B. Benhamou and L. Sais. Theoretical study of symmetries in propositional calculus and applications. In Proc. 11th CADE, Saratoga Springs. Springer, LNCS 607, 1992.","DOI":"10.1007\/3-540-55602-8_172"},{"key":"3_CR3","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"W. Cook, C. R. Coullard, and G. Tur\u00e1n. On the complexity of cutting plane proofs. Discrete Applied Mathematics, 18:25\u201338, 1987.","journal-title":"Discrete Applied Mathematics"},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201\u2013205, 1960.","journal-title":"Journal of the ACM"},{"issue":"2&3","key":"3_CR5","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. Theoretical Computer Science, 39(2 & 3):297\u2013308, 1985.","journal-title":"Theoretical Computer Science"},{"key":"3_CR6","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0167-9236(88)90097-8","volume":"4","author":"J. N. Hooker","year":"1988","unstructured":"J. N. Hooker. A quantitative approach to logical inference. Decision Support Systems, 4:45\u201369, 1988.","journal-title":"Decision Support Systems"},{"issue":"1","key":"3_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","volume":"7","author":"J. N. Hooker","year":"1988","unstructured":"J. N. Hooker. Resolution vs. cutting plane solution of inference problems: some computational experience. Operations Research Letters, 7(1):1\u20137, 1988.","journal-title":"Operations Research Letters"},{"key":"3_CR8","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF01531033","volume":"6","author":"J. N. Hooker","year":"1992","unstructured":"J. N. Hooker. Generalized resolution for 0\u20131 linear inequalities. Annals of Mathematics and Artificial Intelligence, 6:271\u2013286, 1992.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"3_CR9","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BF01531074","volume":"1","author":"J. N. Hooker","year":"1990","unstructured":"J. N. Hooker and C. Fedjki. Branch-and-cut solution of inference problems in propositional logic. Annals of Mathematics and Artificial Intelligence, 1:123\u2013139, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"3_CR10","volume-title":"volume 6 of Fundamental studies in computer science","author":"D. W. Loveland","year":"1978","unstructured":"D. W. Loveland. Automated theorem proving: a logical basis, volume 6 of Fundamental studies in computer science. North-Holland, Amsterdam, 1978."},{"key":"3_CR11","unstructured":"I. Mitterreiter and F. J. Radermacher. Experiments on the running time behaviour of some algorithms solving propositional logic problems. Technical report, FAW Ulm, 1991."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. Series in Discrete Mathematics and Optimization. Wiley-Interscience, 1988.","DOI":"10.1002\/9781118627372"},{"issue":"1","key":"3_CR13","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"J. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, 1965.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Constraints in Computational Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0016842","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T11:43:57Z","timestamp":1683287037000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0016842"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354058403X"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0016842","relation":{},"subject":[]}}