__
Revision #1 to TR23-121 | 20th August 2023 12:01
__
#### Depth d Frege systems are not automatable unless P=NP

**Abstract:**
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 the result of Atserias and Muller [JACM, 2020] for the non-automatability of resolution—a depth 1 Frege system—to any depth $d>0$ Frege system.

**Changes to previous version:**
Some typos fixed, keywords added

__
TR23-121 | 19th August 2023 04:53
__

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

**Abstract:**
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 the result of Atserias and Muller [JACM, 2020] for the non-automatability of resolution—a depth 1 Frege system—to any depth $d>0$ Frege system.