Document Open Access Logo

Towards a Theory of Algorithmic Proof Complexity (Invited Talk)

Author Albert Atserias

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.1.pdf
  • Filesize: 346 kB
  • 2 pages

Document Identifiers

Author Details

Albert Atserias
  • Universitat Politècnica de Catalunya, Centre de Recerca Matemàtica, Barcelona, Spain

Funding

  • Atserias, Albert: Partially funded by Spanish State Research Agency, through the Severo Ochoa and María de Maeztu Program for Centers and Units of Excellence in R&D (CEX2020-001084-M) and Ministerio de Ciencia e Innovación (MICIN) through project PID2019- 109137GB-C22 (PROOFS).

Cite AsGet BibTex

Albert Atserias. Towards a Theory of Algorithmic Proof Complexity (Invited Talk). In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.1

Abstract

A possibly unexpected by-product of the mathematical study of the lengths of proofs, as is done in the field of propositional proof complexity, is, I claim, that it may lead to new polynomial-time algorithms. To explain this, I will first recall the origins of proof complexity as a field, and then explain why some of the recent progress in it could lead to some new algorithms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • logic
  • computational complexity

Metrics

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

References

  1. Miklós Ajtai. The complexity of the pigeonhole principle. Comb., 14(4):417-433, 1994. URL: https://doi.org/10.1007/BF01302964.
  2. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. Prelim. in CCC 2003. URL: https://doi.org/10.1016/j.jcss.2007.06.025.
  3. Albert Atserias and Moritz Müller. Automating resolution is np-hard. J. ACM, 67(5):31:1-31:17, 2020. Prelim. in FOCS 2019. URL: https://doi.org/10.1145/3409472.
  4. Stephen A. Cook. The Complexity of Theorem-Proving Procedures. In STOC, pages 151-158. ACM, 1971. Google Scholar
  5. Stephen A. Cook and Robert A. Reckhow. On the Lengths of Proofs in the Propositional Calculus (Preliminary Version). In Proceedings of the 6th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1974, Seattle, Washington, USA, pages 135-148. ACM, 1974. URL: https://doi.org/10.1145/800119.803893.
  6. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  7. Susanna F. de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, and Dmitry Sokolov. Automating algebraic proof systems is NP-hard. In STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing, Virtual Event, Italy, June 21-25, 2021, pages 209-222. ACM, 2021. URL: https://doi.org/10.1145/3406325.3451080.
  8. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is NP-hard. In Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 68-77. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384248.
  9. Armin Haken. The Intractability of Resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  10. Tuomas Hakoniemi. Size bounds for algebraic and semialgebraic proof systems. PhD thesis, Universitat Politècnica de Catalunya, 2022. Google Scholar
  11. Jan Krajícek, Pavel Pudlák, and Alan R. Woods. An Exponenetioal Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole Principle. Random Struct. Algorithms, 7(1):15-40, 1995. URL: https://doi.org/10.1002/rsa.3240070103.
  12. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential Lower Bounds for the Pigeonhole Principle. Comput. Complex., 3:97-140, 1993. URL: https://doi.org/10.1007/BF01200117.
  13. Pavel Pudlák. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  14. Pavel Pudlák and Samuel R. Buss. How to Lie Without Being (Easily) Convicted and the Length of Proofs in Propositional Calculus. In Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 151-162. Springer, 1994. URL: https://doi.org/10.1007/BFb0022253.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact