{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T05:36:11Z","timestamp":1777354571066,"version":"3.51.4"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,2,14]],"date-time":"2009-02-14T00:00:00Z","timestamp":1234569600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2010,8]]},"DOI":"10.1007\/s00224-009-9195-5","type":"journal-article","created":{"date-parts":[[2009,2,16]],"date-time":"2009-02-16T09:57:14Z","timestamp":1234778234000},"page":"491-506","source":"Crossref","is-referenced-by-count":13,"title":["On the Automatizability of Polynomial Calculus"],"prefix":"10.1007","volume":"47","author":[{"given":"Nicola","family":"Galesi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,2,14]]},"reference":[{"key":"9195_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.A.: Lower bounds for polynomial calculus: Non-binomial case. In: 42nd Annual Symposium on Foundations of Computer Science, pp.\u00a0190\u2013199 (2001)","DOI":"10.1109\/SFCS.2001.959893"},{"issue":"4","key":"9195_CR2","doi-asserted-by":"crossref","first-page":"1347","DOI":"10.1137\/06066850X","volume":"38","author":"M. Alekhnovich","year":"2008","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. SIAM J. Comput. 38(4), 1347\u20131363 (2008)","journal-title":"SIAM J. Comput."},{"key":"9195_CR3","first-page":"1749","volume-title":"Handbook of Combinatorics","author":"N. Alon","year":"1995","unstructured":"Alon, N.: Tools from higher algebra. In: Handbook of Combinatorics, vol.\u00a02, pp. 1749\u20131783. MIT Press, Cambridge (1995)"},{"issue":"2","key":"9195_CR4","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/j.ic.2003.10.004","volume":"189","author":"A. Atserias","year":"2004","unstructured":"Atserias, A., Bonet, M.L.: On the automatizability of resolution and related propositional proof systems. Inf. Comput. 189(2), 182\u2013201 (2004)","journal-title":"Inf. Comput."},{"key":"9195_CR5","first-page":"274","volume-title":"37th Annual Symposium on Foundations of Computer Science","author":"P. Beame","year":"1996","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: 37th Annual Symposium on Foundations of Computer Science, pp.\u00a0274\u2013282. IEEE Press, New York (1996)"},{"key":"9195_CR6","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow\u2014resolution made simple. In: Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, pp.\u00a0517\u2013526 (1999)","DOI":"10.1145\/301250.301392"},{"issue":"1\u20132","key":"9195_CR7","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/s00037-004-0183-5","volume":"13","author":"M.L. Bonet","year":"2004","unstructured":"Bonet, M.L., Domingo, C., Gavald\u00e0, R., Maciel, A., Pitassi, T.: Non-automatizability of bounded-depth frege proofs. Comput. Complex. 13(1\u20132), 47\u201368 (2004)","journal-title":"Comput. Complex."},{"issue":"6","key":"9195_CR8","doi-asserted-by":"crossref","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"M.L. Bonet","year":"2000","unstructured":"Bonet, M.L., Pitassi, T., Raz, R.: On interpolation and automatization for frege systems. SIAM J. Comput. 29(6), 1939\u20131967 (2000)","journal-title":"SIAM J. Comput."},{"key":"9195_CR9","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, pp.\u00a0174\u2013183 (1996)","DOI":"10.1145\/237814.237860"},{"key":"9195_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-35651-8","volume-title":"Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"D. Cox","year":"2007","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra, 3rd edn. Springer, New York (2007)","edition":"3"},{"key":"9195_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0515-9","volume-title":"Parameterized Complexity","author":"R. Downey","year":"1999","unstructured":"Downey, R., Fellows, M.: Parameterized Complexity. Springer, New York (1999)"},{"key":"9195_CR12","unstructured":"Galesi, N., Lauria, M.: Degree lower bounds for a graph ordering principle. Submitted. See http:\/\/www.dsi.uniroma1.it\/~galesi\/publications.html"},{"key":"9195_CR13","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9195_CR14","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/s000370050024","volume":"8","author":"R. Impagliazzo","year":"1999","unstructured":"Impagliazzo, R., Pudl\u00e1k, P., Sgall, J.: Lower bounds for the polynomial calculus and the Gr\u00f6bner basis algorithm. Comput. Complex. 8(2), 127\u2013144 (1999)","journal-title":"Comput. Complex."},{"key":"9195_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04650-0","volume-title":"Extremal Combinatorics: with Applications in Computer Science","author":"S. Jukna","year":"2001","unstructured":"Jukna, S.: Extremal Combinatorics: with Applications in Computer Science. Springer, New York (2001)"},{"issue":"4","key":"9195_CR16","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1002\/1521-3870(200211)48:4<602::AID-MALQ602>3.0.CO;2-J","volume":"48","author":"J. Kraj\u00edcek","year":"2002","unstructured":"Kraj\u00edcek, J.: Interpolation and approximate semantic derivations. Math. Log. Q. 48(4), 602\u2013606 (2002)","journal-title":"Math. Log. Q."},{"key":"9195_CR17","series-title":"Lecture Notes in Computer Science","first-page":"210","volume-title":"LCC","author":"J. Kraj\u00edcek","year":"1994","unstructured":"Kraj\u00edcek, J., Pudl\u00e1k, P.: Some consequences of cryptographical conjectures for S 2 1 and ef. In: Leivant,\u00a0D. (ed.) LCC. Lecture Notes in Computer Science, vol.\u00a0960, pp.\u00a0210\u2013220. Springer, Berlin (1994)"},{"key":"9195_CR18","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","first-page":"215","volume-title":"Descriptive Complexity and Finite Models","author":"T. Pitassi","year":"1996","unstructured":"Pitassi, T.: Algebraic propositional proof systems. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a031, pp.\u00a0215\u2013244. Am. Math. Soc., Providence (1996)"},{"key":"9195_CR19","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1016\/S0304-3975(02)00411-5","volume":"295","author":"P. Pudl\u00e1k","year":"2003","unstructured":"Pudl\u00e1k, P.: On reducibility and symmetry of disjoint np-pairs. Theor. Comput. Sci. 295, 626\u2013638 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"9195_CR20","first-page":"279","volume":"39","author":"P. Pudl\u00e1k","year":"1998","unstructured":"Pudl\u00e1k, P., Sgall, J.: Algebraic models of computation and interpolation for algebraic proof systems. DIMACS Ser. Theor. Comput. Sci. 39, 279\u2013296 (1998)","journal-title":"DIMACS Ser. Theor. Comput. Sci."},{"issue":"4","key":"9195_CR21","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/s000370050013","volume":"7","author":"A.A. Razborov","year":"1998","unstructured":"Razborov, A.A.: Lower bounds for the polynomial calculus. Comput. Complex. 7(4), 291\u2013324 (1998)","journal-title":"Comput. Complex."},{"key":"9195_CR22","series-title":"Graduate Texts in Mathematics","volume-title":"Introduction to Coding Theory","author":"J.H. Lint van","year":"1998","unstructured":"van Lint, J.H.: Introduction to Coding Theory, 3rd edn. Graduate Texts in Mathematics. Springer, New York (1998)","edition":"3"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-009-9195-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-009-9195-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-009-9195-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T11:51:37Z","timestamp":1558698697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-009-9195-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,14]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["9195"],"URL":"https:\/\/doi.org\/10.1007\/s00224-009-9195-5","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2,14]]}}}