A reduction of proof complexity to computational complexity for $AC^0[p]$ Frege systems

AbstractWe investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference, (TABLEAUX’15), pp 185–200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI’17), pp 4919–4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover–Delayer games, which can be used to establish “genuine” modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2–3):194–205, 2009) and obtain a “genuinely” modal separation.

Download Full-text

INCOMPLETENESS IN THE FINITE DOMAIN

Bulletin of Symbolic Logic ◽

10.1017/bsl.2017.32 ◽

2017 ◽

Vol 23 (4) ◽

pp. 405-441 ◽

Cited By ~ 5

Author(s):

PAVEL PUDLÁK

Keyword(s):

Computational Complexity ◽

Proof Complexity ◽

Finite Domain ◽

Semantic Concept ◽

Syntactic Complexity ◽

Special Cases ◽

Incompleteness Theorems ◽

High Computational Complexity

AbstractMotivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyondNP≠coNP. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be special cases of such general statements and we want to formalize and fully understand these statements. Roughly speaking, we are trying to connect syntactic complexity, by which we mean the complexity of sentences and strengths of the theories in which they are provable, with the semantic concept of complexity of the computational problems represented by these sentences.We have introduced the most fundamental conjectures in our earlier works [27, 33–35]. Our aim in this article is to present them in a more systematic way, along with several new conjectures, and prove new connections between them and some other statements studied before.

Download Full-text

The polynomial bounds of proof complexity in Frege systems

Siberian Mathematical Journal ◽

10.1007/s11202-009-0022-7 ◽

2009 ◽

Vol 50 (2) ◽

pp. 193-198 ◽

Cited By ~ 1

Author(s):

S. R. Aleksanyan ◽

A. A. Chubaryan

Keyword(s):

Proof Complexity ◽

Frege Systems ◽

Polynomial Bounds

Download Full-text

Witnessing matrix identities and proof complexity

International Journal of Algebra and Computation ◽

10.1142/s021819671850011x ◽

2018 ◽

Vol 28 (02) ◽

pp. 217-256

Author(s):

Fu Li ◽

Iddo Tzameret

Keyword(s):

Computational Complexity ◽

Lower Bound ◽

Finite Basis ◽

Proof Complexity ◽

Polynomial Identities ◽

Open Problems ◽

Complete Proof ◽

Proof Systems ◽

Matrix Identity ◽

Matrix Identities

We use results from the theory of algebras with polynomial identities (PI-algebras) to study the witness complexity of matrix identities. A matrix identity of [Formula: see text] matrices over a field [Formula: see text]is a non-commutative polynomial (f(x1, …, xn)) over [Formula: see text], such that [Formula: see text] vanishes on every [Formula: see text] matrix assignment to its variables. For every field [Formula: see text]of characteristic 0, every [Formula: see text] and every finite basis of [Formula: see text] matrix identities over [Formula: see text], we show there exists a family of matrix identities [Formula: see text], such that each [Formula: see text] has [Formula: see text] variables and requires at least [Formula: see text] many generators to generate, where the generators are substitution instances of elements from the basis. The lower bound argument uses fundamental results from PI-algebras together with a generalization of the arguments in [P. Hrubeš, How much commutativity is needed to prove polynomial identities? Electronic colloquium on computational complexity, ECCC, Report No.: TR11-088, June 2011].We apply this result in algebraic proof complexity, focusing on proof systems for polynomial identities (PI proofs) which operate with algebraic circuits and whose axioms are the polynomial-ring axioms [P. Hrubeš and I. Tzameret, The proof complexity of polynomial identities, in Proc. 24th Annual IEEE Conf. Computational Complexity, CCC 2009, 15–18 July 2009, Paris, France (2009), pp. 41–51; Short proofs for the determinant identities, SIAM J. Comput. 44(2) (2015) 340–383], and their subsystems. We identify a decrease in strength hierarchy of subsystems of PI proofs, in which the [Formula: see text]th level is a sound and complete proof system for proving [Formula: see text] matrix identities (over a given field). For each level [Formula: see text] in the hierarchy, we establish an [Formula: see text] lower bound on the number of proof-steps needed to prove certain identities.Finally, we present several concrete open problems about non-commutative algebraic circuits and speed-ups in proof complexity, whose solution would establish stronger size lower bounds on PI proofs of matrix identities, and beyond.

Download Full-text

Chapter 7. Proof Complexity and SAT Solving

Frontiers in Artificial Intelligence and Applications - Handbook of Satisfiability ◽

10.3233/faia200990 ◽

2021 ◽

Author(s):

Sam Buss ◽

Jakob Nordström

Keyword(s):

Linear Algebra ◽

Cutting Planes ◽

Proof Complexity ◽

Sat Solving ◽

Proof Systems ◽

Frege Systems ◽

Ample Supply ◽

Clause Learning ◽

Algebraic Approaches ◽

Polynomial Calculus

This chapter gives an overview of proof complexity and connections to SAT solving, focusing on proof systems such as resolution, Nullstellensatz, polynomial calculus, and cutting planes (corresponding to conflict-driven clause learning, algebraic approaches using linear algebra or Gröbner bases, and pseudo-Boolean solving, respectively). There is also a discussion of extended resolution (which is closely related to DRAT proof logging) and Frege and extended Frege systems more generally. An ample supply of references for further reading is provided, including for some topics omitted in this chapter.

Download Full-text

The Complexity of Propositional Proofs

Bulletin of Symbolic Logic ◽

10.2178/bsl/1203350879 ◽

2007 ◽

Vol 13 (4) ◽

pp. 417-481 ◽

Cited By ~ 138

Author(s):

Nathan Segerlind

Keyword(s):

Computational Complexity ◽

Lower Bounds ◽

Proof Complexity ◽

Propositional Proof Complexity ◽

Propositional Proof ◽

Satisfiability Algorithms ◽

Complexity Theories

AbstractPropositional proof complexity is the study of the sizes of propositional proofs, and more generally, the resources necessary to certify propositional tautologies. Questions about proof sizes have connections with computational complexity, theories of arithmetic, and satisfiability algorithms. This is article includes a broad survey of the field, and a technical exposition of some recently developed techniques for proving lower bounds on proof sizes.

Download Full-text