Document Open Access Logo

The Model-Theoretic Expressiveness of Propositional Proof Systems

Authors Erich Grädel, Benedikt Pago, Wied Pakusa

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.27.pdf
  • Filesize: 0.53 MB
  • 18 pages

Document Identifiers

Author Details

Erich Grädel
Benedikt Pago
Wied Pakusa

Cite AsGet BibTex

Erich Grädel, Benedikt Pago, and Wied Pakusa. The Model-Theoretic Expressiveness of Propositional Proof Systems. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.27

Abstract

We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.
Keywords
  • Propositional proof systems
  • fixed-point logics
  • resolution
  • polynomial calculus
  • generalized quantifiers

Metrics

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

References

  1. M. Anderson and A. Dawar. On symmetric circuits and fixed-point logics. In STACS 2014, pages 41-52, 2014. Google Scholar
  2. A. Atserias. On sufficient conditions for unsatisfiability of random formulas. J. ACM, 51(2):281-311, 2004. Google Scholar
  3. A. Atserias, A. Bulatov, and A. Dawar. Affine systems of equations and counting infinitary logic. Theoretical Computer Science, 410:1666-1683, 2009. Google Scholar
  4. A. Atserias and V. Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, 2008. Google Scholar
  5. A. Atserias and E. N. Maneva. Sherali-adams relaxations and indistinguishability in counting logics. In Shafi Goldwasser, editor, Innovations in Theoretical Computer Science 2012, Cambridge, MA, USA, January 8-10, 2012, pages 367-379. ACM, 2012. Google Scholar
  6. L. Babai. Graph isomorphism in quasipolynomial time. CoRR, abs/1512.03547, 2015. URL: http://arxiv.org/abs/1512.03547.
  7. P. Beame and T. Pitassi. Propositional Proof Complexity: Past, Present, and Future. Current Trends in TCS: Entering the 21st Century, pages 42-70, 2001. Google Scholar
  8. E. Ben-Sasson and A. Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  9. C. Berkholz and M. Grohe. Limitations of algebraic approaches to graph isomorphism testing. In Proceedings of ICALP 2015, pages 155-166, 2015. Google Scholar
  10. C. Berkholz and M. Grohe. Linear diophantine equations, group csps, and graph isomorphism. In Proceedings of SODA 2017, pages 327-339, 2017. Google Scholar
  11. J. Cai, M. Fürer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):389-410, 1992. Google Scholar
  12. C. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In STOC 2017, 2017. Google Scholar
  13. M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner Basis Algorithm to find Proofs of Unsatisfiability. In STOC 1996, pages 174-183, 1996. Google Scholar
  14. S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. J. Symbolic Logic, 44:36-50, 1979. Google Scholar
  15. A. Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, 2(1):8-21, 2015. Google Scholar
  16. A. Dawar and E. Grädel. The descriptive complexity of parity games. In Proceedings of CSL 2008, pages 354-368, 2008. Google Scholar
  17. A. Dawar, M. Grohe, B. Holm, and B. Laubner. Logics with rank operators. In LICS 2009, pages 113-122, 2009. Google Scholar
  18. A. Dawar and P. Wang. Lasserre lower bounds and definability of semidefinite programming. CoRR, abs/1602.05409, 2016. Google Scholar
  19. M. R. Garey, D. S. Johnson, and L. Stockmeyer. Some simplified NP-complete graph problems. Theoretical Computer Science, 1(3):237-267, 1976. Google Scholar
  20. E. Grädel and S. Hegselmann. Counting in Team Semantics. In CSL 2016, 2016. Google Scholar
  21. M. Grohe and M. Otto. Pebble games and linear equations. J. Symb. Log., 80(3):797-844, 2015. Google Scholar
  22. P. N. Malkin. Sherali-adams relaxations of graph isomorphism polytopes. Discrete Optimization, 12:73-97, 2014. Google Scholar
  23. M. Otto. Bounded Variable Logics and Counting. Springer, 1997. Google Scholar
  24. W. Pakusa. Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time. PhD thesis, RWTH Aachen University, 2016. Google Scholar
  25. N. Segerlind. The Complexity of Propositional Proofs. Bulletin of Symbolic Logic, 13(04):417-481, 2007. Google Scholar
  26. J. Torán. On the resolution complexity of graph non-isomorphism. In Theory and Applications of Satisfiability Testing - SAT 2013, volume 7962 of LNCS, pages 52-66, 2013. Google Scholar
  27. O. Verbitsky. On the dynamic width of the 3-colorability problem. CoRR, abs/1312.5937, 2013. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact