Abstract | ||
---|---|---|
We investigate the question whether there is a (p-)optimal proof system for SAT or for TAUT and its relation to completeness and collapse results for nondeterministic function classes. A p-optimal proof system for SAT is shown to imply (1) that there exists a complete function for the class of all total nondeterministic multi-valued functions and (2) that any set with an optimal proof system has a p-optimal proof system. By replacingthe assumption of the mere existence of a (p-) optimal proof system by the assumption that certain proof systems are (p-)optimal we obtain stronger consequences, namely collapse results for various function classes. Especially we investigate the question whether the standard proof system for SAT is p-optimal. We show that this assumption is equivalent to a variety of complexity theoretical assertions studied before, and to the assumption that every optimal proof system is p-optimal. Finally, we investigate whether there is an optimal proof system for TAUT that admits an effective interpolation, and show some relations between various completeness assumptions. |
Year | DOI | Venue |
---|---|---|
2000 | 10.1007/3-540-44450-5_29 | FSTTCS |
Keywords | Field | DocType |
optimal proof system,sat p-optimal,nondeterministic function class,various completeness assumption,p-optimal proof system,various function class,total nondeterministic multi-valued function,replacingthe assumption,certain proof system,standard proof system,complete function,value function | Analytic proof,Discrete mathematics,Combinatorics,Existential quantification,Nondeterministic algorithm,Turing machine,Proof complexity,Time complexity,Completeness (statistics),Mathematics,Direct proof | Conference |
Volume | ISSN | ISBN |
1974 | 0302-9743 | 3-540-41413-4 |
Citations | PageRank | References |
10 | 0.63 | 18 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Johannes Köbler | 1 | 580 | 46.51 |
Jochen Messner | 2 | 70 | 4.86 |