[Proof Complexity] Preprint for proof complexity (NP Search Problems for Frege and Extended Frege Proofs)

[Sam Buss]

Dear Colleagues,

A new preprint by Arnold Beckmann and myself "The NP Search Problems for
Frege and Extended Frege Proofs" is available at
http://www.math.ucsd.edu/~sbuss/ResearchWeb/NPsearchFrege/, or directly at
http://www.math.ucsd.edu/~sbuss/ResearchWeb/NPsearchFrege/paper.pdf.

Comments and suggestions are welcomed.

Best regards, Sam

---
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.
---