×
Bonacina, Ilario; Galesi, Nicola

A framework for space complexity in algebraic proof systems. (English) Zbl 1333.03238

J. ACM 62, No. 3, Article No. 23, 20 p. (2015).

Cited in 6 Documents

MSC:

03F20 Complexity of proofs
03B05 Classical propositional logic
03B35 Mechanization of proofs and logical operations
03D15 Complexity of computation (including implicit computational complexity)
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

proof complexity; algebraic proof systems; polynomial calculus; random formulae; resolution; space complexity

Citations:

Zbl 1004.03047; Zbl 1372.03099
Cite Review PDF
Full Text: DOI

References:

[1] Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. 2002. Space complexity in propositional calculus. SIAM J. Comput. 31, 4, 1184–1211. · Zbl 1004.03047 · doi:10.1137/S0097539700366735
[2] Michael Alekhnovich and Alexander A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings of the Steklov Institute of Mathematics, Vol. 242. 18–35. · Zbl 1079.03047
[3] Albert Atserias. 2004. On sufficient conditions for unsatisfiability of random formulas. J. ACM 51, 2, 281–311. · Zbl 1316.68055 · doi:10.1145/972639.972645
[4] Albert Atserias and Víctor Dalmau. 2008. A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74, 3, 323–334. · Zbl 1133.03034 · doi:10.1016/j.jcss.2007.06.025
[5] Paul Beame and Toniann Pitassi. 1996. Simplified and improved resolution lower bounds. In Proceedings of FOCS. IEEE Computer Society, 274–282. · Zbl 0866.03029 · doi:10.1109/SFCS.1996.548486
[6] Eli Ben-Sasson. 2001. Expansion in proof complexity. Ph.D. dissertation, Hebrew University.
[7] Eli Ben-Sasson and Nicola Galesi. 2003. Space complexity of random formulae in resolution. Random Struct. Algorithms 23, 1, 92–109. · Zbl 1048.03046 · doi:10.1002/rsa.10089
[8] Eli Ben-Sasson and Russell Impagliazzo. 2010. Random CNF’s are hard for the polynomial calculus. Computat. Complex. 19, 4, 501–519. · Zbl 1216.03064 · doi:10.1007/s00037-010-0293-1
[9] Eli Ben-Sasson and Jakob Nordström. 2011. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of ICS, Bernard Chazelle (Ed.), Tsinghua University Press, 401–416.
[10] Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow - Resolution made simple. J. ACM 48, 2, 149–169. · Zbl 1089.03507 · doi:10.1145/375827.375835
[11] Patrick Bennet, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan. 2015. Space proof complexity for random 3-CNFs. arXiv. (2015) http://arxiv.org/abs/1503.01613. · Zbl 1423.03242
[12] Archie Blake. 1937. Canonical expressions in Boolean algebra. Ph.D. dissertation, University of Chicago. · Zbl 0018.38601
[13] Ilario Bonacina and Nicola Galesi. 2013. Pseudo-partitions, transversality and locality: A combinatorial characterization for the space measure in algebraic proof systems. In Proceedings of ITCS. Robert D. Kleinberg (Ed.), ACM, 455–472. · Zbl 1364.03081 · doi:10.1145/2422436.2422486
[14] Ilario Bonacina, Nicola Galesi, and Neil Thapen. 2014. Total space in resolution. In Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS). 641–650. · Zbl 1402.03080 · doi:10.1109/FOCS.2014.74
[15] Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. 2001. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci. 62, 2, 267–289. · Zbl 1007.03052 · doi:10.1006/jcss.2000.1726
[16] Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiri Sgall. 1997. Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Computat. Complex. 6, 3, 256–298. · Zbl 0890.03030 · doi:10.1007/BF01294258
[17] Vasek Chvátal and Endre Szemerédi. 1988. Many hard examples for resolution. J. ACM 35, 4, 759–768. · Zbl 0712.03008 · doi:10.1145/48014.48016
[18] Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. 1996. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of STOC. Gary L. Miller (Ed.), ACM, 174–183. · Zbl 0938.68825 · doi:10.1145/237814.237860
[19] Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symb. Log. 44, 1, 36–50. · Zbl 0408.03044 · doi:10.2307/2273702
[20] David A. Cox, John Little, and Donal O’Shea. 1997. Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra 2nd Ed., Springer. I–XIII, 1–536. · Zbl 0861.13012
[21] Juan Luis Esteban, Nicola Galesi, and Jochen Messner. 2004. On the complexity of resolution with bounded conjunctions. Theoret. Comput. Sci. 321, 2–3, 347–370. · Zbl 1056.03036 · doi:10.1016/j.tcs.2004.04.004
[22] Juan Luis Esteban and Jacobo Torán. 2001. Space bounds for resolution. Inf. Comput. 171, 1, 84–97. · Zbl 1005.03009 · doi:10.1006/inco.2001.2921
[23] Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. 2013. Towards an understanding of polynomial calculus: New separations and lower bounds - (Extended Abstract). In Proceedings of ICALP (1), Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg (Eds.), (Lecture Notes in Computer Science) vol. 7965, Springer, 437–448. · Zbl 1336.03065
[24] Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga Ron-Zewi. 2012. Space complexity in polynomial calculus. In Proceedings of IEEE Conference on Computational Complexity. IEEE, 334–344. · doi:10.1109/CCC.2012.27
[25] Nicola Galesi and Massimo Lauria. 2010a. On the automatizability of polynomial calculus. Theory Comput. Syst. 47, 2, 491–506. · Zbl 1211.03025 · doi:10.1007/s00224-009-9195-5
[26] Nicola Galesi and Massimo Lauria. 2010b. Optimality of size-degree tradeoffs for polynomial calculus. ACM Trans. Comput. Log. 12, 1, 4. · Zbl 1352.03066
[27] Russell Impagliazzo, Pavel Pudlák, and Jiri Sgall. 1999. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complex. 8, 2, 127–144. · Zbl 0946.68129 · doi:10.1007/s000370050024
[28] Jan Krajíček. 2009. Propositional proof complexity I. Manuscript available at author’s webpage.
[29] Jakob Nordström. 2009. Narrow proofs may be spacious: Separating space and width in resolution. SIAM J. Comput. 39, 1, 59–121. · Zbl 1192.03042 · doi:10.1137/060668250
[30] Jakob Nordström and Johan Håstad. 2013. Towards an optimal separation of space and length in resolution. Theory Comput. 9, 471–557. · Zbl 1366.68098 · doi:10.4086/toc.2013.v009a014
[31] Pavel Pudlák and Jiří Sgall. 1998. Algebraic models of computation and interpolation for algebraic proof systems. DIMACS Series in Discrete Math. Theoret. Comput. Sci. 39, 279–295. · Zbl 0901.03033
[32] Alexander A. Razborov. 1998. Lower bounds for the polynomial calculus. Computat. Complex. 7, 4, 291–324. · Zbl 1026.03043 · doi:10.1007/s000370050013
[33] Alexander A. Razborov. 2003. Pseudorandom generators hard fork-DNF resolution and polynomial calculus resolution. Manuscript available at author’s webpage. · Zbl 1376.03055
[34] John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1, 23–41. · Zbl 0139.12303 · doi:10.1145/321250.321253
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.