Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size

Susanna F. de Rezende, David Engström, Yassine Ghannane +1

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) \l…