Optimal Proof Systems, Optimal Acceptors and Recursive Presentability

• Autorzy: Sadowski Z.
• Języki publikacji: EN

Abstrakty

EN

We advocate the thesis that the following general statements are equivalent: the existence of an optimal proof system, the existence of an optimal acceptor (an algorithm with optimality property stated only for input strings which are accepted), and the existence of a suitable recursive presentation of the class of all easy (polynomial-time recognizable) subsets of TAUT (SAT). We prove three concrete versions of this thesis with different variants of notions appearing in it. These versions give alternative characterizations of the following problems: the existence of a p-optimal proof system for SAT, the existence of an optimal proof system for TAUT, and the existence of an optimal and automatizable proof system for TAUT.

Słowa kluczowe

EN

abstract propositional proof systems; automatizable proof systems; recursive presentability; disjoint NP-pairs

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 1-2
• Strony: 169--185
• Opis fizyczny: bibliogr. 25 poz.

Twórcy

autor

Sadowski Z.

• Institute of Mathematics, University of Białystok, Akademicka 2, 15-267 Białystok, Poland,

Bibliografia

• [1] Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate, Journal of Symbolic Logic, 66, 2001, 171 - 191.
• [2] Bálcazar, J. L., Dıaz, J., Gabarró, J.: Structural complexity I, 2nd ed., Springer-Verlag, 1995.
• [3] Beyersdorff, O.: Disjoint NP-Pairs and Propositional Proof Systems, PhD Thesis, Humboldt-Universität zu Berlin, July 2006.
• [4] Bonet, M. L, Pitassi, T., Raz, R.: On interpolation and automatization for Frege systems, SIAM Journal on Computing, 29 (6), 2000, 1939 -1967.
• [5] Buhrman, H., Fenner, S., Fortnow, L., van Melkebeek,D.: Optimal proof systems and sparse sets, Proc. Symposium on Theoretical Aspects of Computer Science, LNCS 1770, Springer - Verlag, Berlin, 2000.
• [6] Cook, S. A., Reckhow R. A. : The relative efficiency of propositional proof systems, Journal of Symbolic Logic, 44, 1979, 36 - 50.
• [7] Fenner, S., Fortnow, L., Naik, A., Rogers J.: On inverting onto functions, Information and Computation, 186 (1), 2003, 90 - 103.
• [8] Glasser, C., Selman, A. L., Sengupta, S.: Reductions between Disjoint NP-Pairs, Information and Computation, 200(2), 2005, 247 - 267.
• [9] Glasser, C., Selman, A. L., Zhang, L.: Canonical disjoint NP-Pairs of propositional proof systems, Theoretical Computer Science, 370(1 - 3), 2007, 60 - 73.
• [10] Grollman, J., Selman, A. L.: Complexity Measures for Public-Key Cryptosystems, SIAM Journal on Computing 17(2), 1988, 309 - 355.
• [11] Hartmanis, J.: On the Importance of Being _2-Hard, Bulletin of the EATCS, 37, 1989, 117 - 127.
• [12] Hartmanis, J., Hemachandra, L.: Complexity classes without machines: On complete languages for UP, Theoretical Computer Science 58, 1988, 129 - 142.
• [13] Kowalczyk, W.: Some connections between presentability of complexity classes and the power of formal systems of reasoning, Proc. Mathematical Foundations of Computer Science, LNCS 176, Springer-Verlag, Berlin, 1988.
• [14] Köbler, J., Messner, J.: Is the standard proof system for SAT p-optimal?, Proc. Foundations of Software Technology and Theoretical Computer Science, LNCS 2136, Springer-Verlag, Berlin, 2001.
• [15] Köbler, J.,Messner, J., Torán, J.: Optimal proof systems imply complete sets for promise classes, Information and Computation textbf184, 2003, 71 - 92.
• [16] Krajıček, J., Pudlák, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations, Journal of Symbolic Logic, 54, 1989, 1063 - 1079.
• [17] Messner, J., On optimal algorithms and optimal proof systems, Proc. Symposium on Theoretical Aspects of Computer Science, LNCS 1563, Springer - Verlag, Berlin, 1999.
• [18] Papadimitriou, C.: Computational Complexity, Addison - Wesley, 1994.
• [19] Pudlák, P.: On reducibility and symmetry of disjoint NP-pairs, Theoretical Computer Science, 295, 2003, 181 - 193.
• [20] Razborov, A.: On provably disjoint NP-pairs, Technical Report 94-006, Electronic Colloquium on Computational Complexity, 1994.
• [21] Sadowski, Z.: On an Optimal Deterministic Algorithm for SAT, Proc. Computer Science Logic (G. Gottlob, E. Grandjean, K. Seyr eds.), LNCS 1584, Springer-Verlag, Berlin, 1999.
• [22] Sadowski, Z.: On a P-optimal Proof System for The Set of All Satisfiable Boolean Formulas (SAT), Proc. Machines, Computations, and Universality (M.Margenstern, Y. Rogozhin eds.), LNCS 2055, Springer-Verlag, Berlin, 2001.
• [23] Sadowski, Z.: On an optimal propositional proof system and the structure of easy subsets of TAUT, Theoretical Computer Science, 288 (1), 2002, 181 - 193.
• [24] Sadowski, Z., On a D-N-optimal acceptor for TAUT, ReportNo. 77, Electronic Colloquiumon Computational Complexity, 2005.
• [25] Schöning, U.: A Uniform Approach to Obtain Diagonal Sets in Complexity Classes, Theoretical Computer Science, 18, 1982, 95 - 103.