{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:26Z","timestamp":1725512006831},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_26","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T08:04:57Z","timestamp":1210061097000},"page":"277-290","source":"Crossref","is-referenced-by-count":1,"title":["Regular and General Resolution: An Improved Separation"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Urquhart","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-1-4899-5327-8_25","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part 2","author":"G. Tseitin","year":"1970","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115\u2013125. Consultants Bureau, New York (1970); Reprinted in[15], vol. 2, pp. 466-483"},{"key":"26_CR2","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the Association for Computing Machinery\u00a05, 394\u2013397 (1962); Reprinted in [15], vol. 1, pp. 267-270","journal-title":"Communications of the Association for Computing Machinery"},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. The Bulletin of Symbolic Logic\u00a01, 425\u2013467 (1995)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"836","DOI":"10.1137\/0216054","volume":"16","author":"W. Huang","year":"1987","unstructured":"Huang, W., Yu, X.: A DNF without regular shortest consensus path. SIAM Journal on Computing\u00a016, 836\u2013840 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1137\/0222044","volume":"22","author":"A. Goerdt","year":"1993","unstructured":"Goerdt, A.: Regular resolution versus unrestricted resolution. SIAM Journal on Computing\u00a022, 661\u2013683 (1993)","journal-title":"SIAM Journal on Computing"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"81","DOI":"10.4086\/toc.2007.v003a005","volume":"3","author":"M. Alekhnovich","year":"2007","unstructured":"Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory of Computing\u00a03, 81\u2013102 (2007); Preliminary version. In: Proceedings of the 34th Annual ACM Symposium on Theory of Computing, May 19-21, 2002, Montr\u00e9al, Qu\u00e9bec, Canada (2002)","journal-title":"Theory of Computing"},{"key":"#cr-split#-26_CR7.1","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of tree-like and general resolution. Combinatorica, 585\u2013603 (2004);","DOI":"10.1007\/s00493-004-0036-5"},{"key":"#cr-split#-26_CR7.2","doi-asserted-by":"crossref","unstructured":"Preliminary version, ECCC TR00-005 (2000)","DOI":"10.1088\/1126-6708\/2000\/03\/005"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B. Krishnamurthy","year":"1985","unstructured":"Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica\u00a022, 253\u2013275 (1985)","journal-title":"Acta Informatica"},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s002360050044","volume":"33","author":"G. St\u00e5lmarck","year":"1996","unstructured":"St\u00e5lmarck, G.: Short resolution proofs for a sequence of tricky formulas. Acta Informatica\u00a033, 277\u2013280 (1996)","journal-title":"Acta Informatica"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s000370100000","volume":"10","author":"M.L. Bonet","year":"2001","unstructured":"Bonet, M.L., Galesi, N.: Optimality of size-width tradeoffs for resolution. Computational Complexity\u00a010, 261\u2013276 (2001); Preliminary version: Proceedings 40th FOCS (1999)","journal-title":"Computational Complexity"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E.: Size Space Tradeoffs For Resolution. In: Proceedings of the 34th ACM Symposium on the Theory of Computing, pp. 457\u2013464 (2002)","DOI":"10.1145\/509907.509975"},{"key":"26_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1002\/rsa.3240070105","volume":"7","author":"A. Kamath","year":"1995","unstructured":"Kamath, A., Motwani, R., Palem, K., Spirakis, P.: Tail bounds for occupancy and the satisfiability threshold conjecture. Random Structures and Algorithms\u00a07, 59\u201380 (1995)","journal-title":"Random Structures and Algorithms"},{"key":"26_CR13","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-662-12788-9_6","volume-title":"Probabilistic Methods for Algorithmic Discrete Mathematics","author":"C. McDiarmid","year":"1998","unstructured":"McDiarmid, C.: Concentration. In: Habib, M., McDiarmid, C., Ramirez-Alfonsin, J., Reed, B. (eds.) Probabilistic Methods for Algorithmic Discrete Mathematics, vol.\u00a016, pp. 195\u2013248. Springer, Heidelberg (1998); Algorithms and Combinatorics 16"},{"key":"26_CR14","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF01683275","volume":"10","author":"W. Paul","year":"1977","unstructured":"Paul, W., Tarjan, R., Celoni, J.: Space bounds for a game on graphs. Mathematical Systems Theory\u00a010, 239\u2013251 (1977)","journal-title":"Mathematical Systems Theory"},{"volume-title":"Automation of Reasoning","year":"1983","key":"26_CR15","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, New York (1983)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:29:15Z","timestamp":1619522955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_26","relation":{},"subject":[]}}