Name
Abstract | ||
|---|---|---|
A polynomial time computable function h : Σ* → Σ* whose range is a set L is called a proof system for L. In this setting, an h-proof for x ∈ L is just a string w with h(w) = x. Cook and Reckhow defined this concept in [13], and in order to compare the relative strength of different proof systems for the set TAUT of tautologies in propositional logic, they considered the notion of p-simulation. Intuitively, a proof system h' p-simulates h if any h-proof w can be translated in polynomial time into an h'-proof w' for h(w). We also consider the related notion of simulation between proof systems where it is only required that for any h-proof w there exists an h'-proof w' whose size is polynomially bounded in the size of w. A proof system is called (p-)optimal for a set L if it (p-)simulates every other proof system for L. The question whether p-optimal or optimal proof systems for TAUT exist is an important one in the field. In this paper we show a close connection between the existence of (p-)optimal proof systems and the existence of complete problems for certain promise complexity classes like UP, NP ∩ Sparse, RP or BPP. For this we introduce the notion of a test set for a promise class C and prove that C has a many-one complete set if and only if C has a test set T with a p-optimal proof system. If in addition the machines defining a promise class have a certain ability to guess proofs, then the existence of a p-optimal proof system for T can be replaced by the presumably weaker assumption that T has an optimal proof system. Strengthening a result from Krajícek and Pudlák [20], we also give sufficient conditions for the existence of optimal and p-optimal proof systems. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1016/S0890-5401(03)00058-0 | Inf. Comput. |
Keywords | Field | DocType |
optimal proof system,p-optimal proof system,optimal proof systems,complete sets,many-one complete set,set l,p-simulates h,proof w,promise class,proof system h,different proof system,h-proof w,proof system | Analytic proof,Probabilistically checkable proof,Discrete mathematics,Combinatorics,Proof by contradiction,Furstenberg's proof of the infinitude of primes,Proof theory,Combinatorial proof,Proof complexity,Mathematics,Direct proof | Journal |
Volume | Issue | ISSN |
184 | 1 | Information and Computation |
Citations | PageRank | References |
25 | 0.94 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Johannes Köbler | 1 | 580 | 46.51 |
| Jochen Messner | 2 | 70 | 4.86 |
| Jacobo Torán | 3 | 564 | 49.26 |