[Proof Complexity] Preprint for proof complexity (NP Search Problems for Frege and Extended Frege Proofs)
Sam Buss
sbuss at ucsd.edu
Tue Mar 1 06:28:53 CET 2016
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.
---
More information about the Proof-Complexity
mailing list