The NP Search Problems of Frege and Extended Frege Proofs
Copyright policy )The NP Search Problems of Frege and Extended Frege Proofs
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.
- University of California, San Diego United States
- Swansea University United Kingdom
Complexity of proofs, First-order arithmetic and fragments, NP search problems, bounded arithmetic, total functions, propositional logic, Frege proofs, proof complexity, extended Frege proofs
Complexity of proofs, First-order arithmetic and fragments, NP search problems, bounded arithmetic, total functions, propositional logic, Frege proofs, proof complexity, extended Frege proofs
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).32 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!