All reports by Author Theodoros Papamakarios:

__
TR23-121
| 19th August 2023
__

Theodoros Papamakarios#### Depth d Frege systems are not automatable unless P=NP

Revisions: 1

__
TR21-176
| 30th November 2021
__

Theodoros Papamakarios#### A super-polynomial separation between resolution and cut-free sequent calculus

__
TR21-074
| 3rd June 2021
__

Theodoros Papamakarios, Alexander Razborov#### Space characterizations of complexity measures and size-space trade-offs in propositional proof systems

Theodoros Papamakarios

We show that for any integer $d>0$, depth $d$ Frege systems are NP-hard to automate. Namely, given a set $S$ of depth $d$ formulas, it is NP-hard to find a depth $d$ Frege refutation of $S$ in time polynomial in the size of the shortest such a refutation. This extends ... more >>>

Theodoros Papamakarios

We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, for the first time, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus ... more >>>

Theodoros Papamakarios, Alexander Razborov

We identify two new big clusters of proof complexity measures equivalent up to

polynomial and $\log n$ factors. The first cluster contains, among others,

the logarithm of tree-like resolution size, regularized (that is, multiplied

by the logarithm of proof length) clause and monomial space, and clause

space, both ordinary and ...
more >>>