Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size
2026-04-30 • Computational Complexity
Computational Complexity
AI summaryⓘ
The authors show that for certain logical formulas, any attempt to prove them false using a specific kind of structured proof system called tree-like Frege with limited complexity must take a very long time—longer than any polynomial in the formula size. They construct explicit examples where the proofs are guaranteed to be super-polynomially long. Their results also extend to related proof systems like degree-d threshold proofs and other semantic tree-like systems with bounded line counts. This means these proof systems have intrinsic limitations in efficiently handling these formulas.
tree-like Frege systemsemantic proof systemCNF formulaproof length lower boundthreshold proof systemdegree-d thresholdsuperpolynomialrefutationline sizeexplicit formula family
Authors
Susanna F. de Rezende, David Engström, Yassine Ghannane, Kilian Risse
Abstract
We prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\varepsilon} \leq s(n) \leq 2^{n^{1-\varepsilon}}$ we exhibit an explicit family $\mathcal{A}$ of $n$-variate CNF formulas $A$, each of size $|A| \le s(n)^{1+\varepsilon}$, such that if $A$ is chosen uniformly from $\mathcal{A}$, then asymptotically almost surely any tree-like Frege refutation of $A$ in line-size $s(n)$ is of length super-polynomial in $|A|$. Our lower bounds apply also to tree-like degree-$d$ threshold systems, for $d \approx \log\bigl(s(n)\bigr)$, that is, for $d$ up to $n^{1-\varepsilon}$. More generally, our lower bounds apply to the semantic version of these systems and to any semantic tree-like proof system where the number of distinct lines is bounded by $\exp\bigl(s(n)\bigr)$.