Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR23-121 | 20th August 2023 12:01

Depth d Frege systems are not automatable unless P=NP

RSS-Feed




Revision #1
Authors: Theodoros Papamakarios
Accepted on: 20th August 2023 12:01
Downloads: 358
Keywords: 


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


Paper:

TR23-121 | 19th August 2023 04:53

Depth d Frege systems are not automatable unless P=NP





TR23-121
Authors: Theodoros Papamakarios
Publication: 20th August 2023 04:12
Downloads: 259
Keywords: 


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.



ISSN 1433-8092 | Imprint