arnold beckmann's pages

The NP Search Problems of Frege and Extended Frege Proofs

File: PDF-File

Author: Arnold Beckmann and Sam Buss
Title: The NP Search Problems of Frege and Extended Frege Proofs
Journal: ACM TOCL 2017, 18(2): 11:1-11:19
Year: 2017
Pages: 19
DOI: 10.1145/3060145

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.

websites: Arnold Beckmann 2017-08-28 Valid HTML 4.01! Valid CSS!