__Preprint:__

**
Arnold Beckmann, Sam Buss
"The NP Search Problems of
Frege and Extended Frege Proofs"
ACM Transactions on Computational Logic,
18, 2 (2017) Article 11.
**

**
Download
preprint.
**

**Abstract:**
We study consistency search problems
for Frege and extended Frege proofs, namely
the NP search problems of finding
syntactic errors in
Frege and extended Frege proofs of contradictions. The
input is a polynomial time function,
or an oracle, describing a proof of a
contradiction; the output is the location of
a syntactic error in the
proof.
The consistency search problems
for Frege and extended Frege systems
are shown to be many-one complete for
the provably total NP search problems of the
second order bounded
arithmetic theories U^1_2 and V^1_2,
respectively.