Document Open Access Logo

A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus

Author Theodoros Papamakarios

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2023.74.pdf
  • Filesize: 0.65 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Resolution
  • Cut-free LK

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, for the first time, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Our super-polynomial separation between resolution and cut-free sequent calculus only applies when clauses are seen as disjunctions of unbounded arity; our examples have linear size cut-free sequent calculus proofs writing, in a particular way, their clauses using binary disjunctions. Interestingly, this shows that the complexity of sequent calculus depends on how disjunctions are represented.

Cite As Get BibTex

Theodoros Papamakarios. A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.74

Author Details

Theodoros Papamakarios
  • Department of Computer Science, University of Chicago, IL, USA

Acknowledgements

We wish to thank Alexander Razborov for numerous suggestions and remarks that greatly improved the presentation of the paper.

References

  1. Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM J. of Computing, 31:1184-1211, 2002. Google Scholar
  2. Noriko Arai. Relative efficency of propositional proof systems: resolution vs. cut-free LK. Annals of Pure and Applied Logic, 104:3-16, 2000. Google Scholar
  3. Noriko Arai, Toniann Pitassi, and Alasdair Urquhart. The complexity of analytic tableaux. J. of Symbolic Logic, 71:777-790, 2006. Google Scholar
  4. Albert Atserias and Victor Dalmau. A combinatorial characterization of resolution width. J. of Computer and System Sciences, 74:323-334, 2008. Google Scholar
  5. Eli Ben-Sasson and Nicola Galesi. Space complexity of random formulae in resolution. Random Structures & Algorithms, 23:92-109, 2003. Google Scholar
  6. Eli Ben-Sasson and Jakob Nordström. Short proofs may be spacious: An optimal separation of space and length in resolution. In Pr. of the 49th Annual IEEE Symp. on Foundations of Computer Science, pages 709-718, 2008. Google Scholar
  7. Eli Ben-Sasson and Jakob Nordström. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Pr. of the 2nd Symp. on Innovations in Computer Science, pages 401-416, 2011. Google Scholar
  8. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. of the ACM, 48:149-169, 2001. Google Scholar
  9. Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan. Space proof complexity for random 3-cnfs. Information and Computation, 255:165-176, 2017. Google Scholar
  10. Ilario Bonacina. Total space in resolution is at least width squared. In Pr. of the 43rd International Colloquium on Automata, Languages, and Programming, pages 56:1-56:13, 2016. Google Scholar
  11. Ilario Bonacina and Nicola Galesi. Pseudo-partitions, transversality and locality: a combinatorial characterization for the space measure in algebraic proof systems. In Pr. of the 4th Conf. on Innovations in Theoretical Computer Science, pages 455-472, 2013. Google Scholar
  12. Ilario Bonacina and Nicola Galesi. A framework for space complexity in algebraic proof systems. J. of the ACM, 62:23:1-23:20, 2015. Google Scholar
  13. Stephen Cook and Robert Reckhow. On the lengths of proofs in the propositional calculus (pr. ver.). In Pr. of the 6th Annual ACM Symp. on Theory of Computing, pages 135-148, 1974. Google Scholar
  14. Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theoretical Computer Science, 321:347-370, 2004. Google Scholar
  15. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171:84-97, 2001. Google Scholar
  16. Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract). In Pr. of the 40th International Colloquium on Automata, Languages, and Programming, pages 437-448, 2013. Google Scholar
  17. Nicola Galesi, Leszek Kołodziejczyk, and Neil Thapen. Polynomial calculus space and resolution width. In Pr. of the 60th Annual IEEE Symp. on Foundations of Computer Science, pages 1325-1337, 2019. Google Scholar
  18. Trinh Huynh and Jakob Nordström. On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity. In Pr. of the 44th Annual ACM Symp. on Theory of Computing, pages 233-248, 2012. Google Scholar
  19. Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. J. of Symbolic Logic, 59:73-86, 1994. Google Scholar
  20. Theodoros Papamakarios and Alexander Razborov. Space characterizations of complexity measures and size-space trade-offs in propositional proof systems. J. of Computer and System Sciences, 137:20-36, 2023. Google Scholar
  21. Robert Reckhow. On the lengths of proofs in the propositional calculus. PhD thesis, Department of Computer Science, University of Toronto, 1975. Google Scholar
  22. Nathan Segerlind, Samuel Buss, and Russell Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM J. of Computing, 33:1171-1200, 2004. Google Scholar
  23. Raymond Smullyan. First-order Logic. Dover, 1995. Google Scholar
  24. Grigori Tseitin. On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic, part 2, pages 115-125, 1968. Google Scholar
  25. Alasdair Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic, 1:425-467, 1995. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact