Arnold Beckmann, Sam Buss
"The NP Search Problems of Frege and Extended Frege Proofs"
ACM Transactions on Computational Logic, 18, 2 (2017) Article 11.
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.
Back to Sam Buss's publications page.