The NP Search Problems of Frege and Extended Frege Proofs

作者：Beckmann Arnold^*; Buss Sam

来源：ACM Transactions on Computational Logic, 2017, 18(2): 11.

DOI：10.1145/3060145

• Bounded arithmetic
• Frege proofs
• extended Frege proofs
• NP search problems
• propositional logic
• total functions
• proof complexity

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-2(1) and V-2(1), respectively.

• 出版日期2017-6