Abstract
A proof system for a language L is a function f such that Range(f) is exactly L. In this article, we look at proof systems from a circuit complexity point of view and study proof systems that are computationally very restricted. The restriction we study is proof systems that can be computed by bounded fanin circuits of constant depth (NC0) or of O(log log n) depth but with O(1) alternations (poly log AC0). Each output bit depends on very few input bits; thus such proof systems correspond to a kind of local error correction on a theorem-proof pair.
We identify exactly how much power we need for proof systems to capture all regular languages. We show that all regular languages have poly log AC0 proof systems, and from a previous result (Beyersdorff et al. [2011a], where NC0 proof systems were first introduced), this is tight. Our technique also shows that Maj has poly log AC0 proof system.
We explore the question of whether Taut has NC0 proof systems. Addressing this question about 2TAUT, and since 2TAUT is closely related to reachability in graphs, we ask the same question about Reachability. We show that if Directed reachability has NC0 proof systems, then so does 2TAUT. We then show that both Undirected Reachability and Directed UnReachability have NC0 proof systems, but Directed Reachability is still open.
In the context of how much power is needed for proof systems for languages in NP, we observe that proof systems for a good fraction of languages in NP do not need the full power of AC0; they have SAC0 or coSAC0 proof systems.
- D. A. Barrington. 1989. Bounded-width polynomial size branching programs recognize exactly those languages in NC1. J. Comput. Syst. Sci. 38 (1989), 150--164. Google ScholarDigital Library
- D. A. Barrington and D. Thérien. 1988. Finite monoids and the fine structure of NC1. J. Assoc. Comput. Mach. 35 (1988), 941--952. Google ScholarDigital Library
- Paul Beame and Toniann Pitassi. 2001. Propositional proof complexity: Past, present, and future. In Current Trends in Theoretical Computer Science: Entering the 21st Century, G. Paun, G. Rozenberg, and A. Salomaa (Eds.). World Scientific Publishing, 42--70. Google ScholarDigital Library
- F. Bedard, F. Lemieux, and P. McKenzie. 1993. Extensions to Barrington’s M-program model. Theor. Comput. Sci. 107 (1993), 31--61. Google ScholarDigital Library
- Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, and Heribert Vollmer. 2013. Verifying proofs in constant depth. ACM Trans. Comput. Theor. 5, 1, Article 2 (May 2013), 23 pages. DOI:http://dx.doi.org/10.1145/2462896.2462898 Google ScholarDigital Library
- Olaf Beyersdorff, Samir Datta, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, and Heribert Vollmer. 2011a. Verifying proofs in constant depth. In Proceedings of 36th Mathematical Foundations of Computer Science Symposium (MFCS). Lecture Notes in Computer Science, Vol. 6907. Springer, 84--95. Google ScholarDigital Library
- Olaf Beyersdorff, Johannes Köbler, and Sebastian Müller. 2011b. Proof systems that take advice. Inform. Comput. 209, 3 (2011), 320--332. Google ScholarDigital Library
- A. Borodin, S. A. Cook, P. W. Dymond, W. L. Ruzzo, and M. Tompa. 1989. Two applications of inductive counting for complementation problems. SIAM J. Comput. 18, 3 (June 1989), 559--578. DOI:http://dx.doi.org/10.1137/0218038 Google ScholarDigital Library
- Stephen A. Cook. 1971. The complexity of theorem-proving procedures. In Proceedings of the Annual Symposium on Theory of Computing (STOC). ACM, 151--158. Google ScholarDigital Library
- Stephen A. Cook and Jan Krajíček. 2007. Consequences of the provability of NP ⊆ P/poly. J. Symbol. Logic 72, 4 (2007), 1353--1371. Google ScholarCross Ref
- Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (1979), 36--50. Google ScholarCross Ref
- Mary Cryan and Peter Bro Miltersen. 2001. On pseudorandom generators in NC0. In Proceedings of 26th Symposium on Mathematical Foundations of Computer Science (MFCS). Springer, Marianske Lazne, Czech Republic, 272--284. Google ScholarDigital Library
- Merrick L. Furst, James B. Saxe, and Michael Sipser. 1984. Parity, circuits, and the polynomial-time hierarchy. Math. Syst. Theor. 17, 1 (1984), 13--27. Google ScholarCross Ref
- Igor Grunsky, Oleksiy Kurganskyy, and Igor Potapov. 2006. On a maximal NFA without mergible states. In Proceecings of the Computer Science Symposium in Russia (CSR). Lecture Notes in Computer Science, Vol. 3967. Springer, 202--210. Google ScholarDigital Library
- Johan Håstad. 1986. Almost optimal lower bounds for small depth circuits. In Proceedings of the 18th Symposium on Theory of Computing (STOC). IEEE Computer Society, 6--20. Google ScholarDigital Library
- Edward A. Hirsch. 2010. Optimal acceptors and optimal proof systems. In Theory and Applications of Models of Computation (TAMC), Jan Kratochvl, Angsheng Li, Ji Fiala, and Petr Kolman (Eds.). Lecture Notes in Computer Science, Vol. 6108. Springer, Berlin, 28--39. DOI:http://dx.doi.org/10.1007/978-3-642-13562-0_4 Google ScholarDigital Library
- Edward A. Hirsch and Dmitry Itsykson. 2010. On optimal heuristic randomized semidecision procedures, with application to proof complexity. In Proceedings of the of 27th Annual Symposium on Theoretical Aspects of Computer Science (STACS) (LIPIcs), Vol. 5. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 453--464.Google Scholar
- John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley. Google ScholarDigital Library
- N. Immerman. 1988. Nondeterministic space is closed under complementation. SIAM J. Comput. 17, 5 (1988), 935--938. DOI:http://dx.doi.org/10.1137/0217058 Google ScholarDigital Library
- J. Justesen. 1972. Class of constructive asymptotically good algebraic codes. IEEE Trans. Inform. Theor. 18, 5 (1972), 652--656. DOI:http://dx.doi.org/10.1109/TIT.1972.1054893 Google ScholarDigital Library
- Andreas Krebs and Nutan Limaye. 2013. DLOGTIME proof systems. In FSTTCS (LIPIcs), Anil Seth and Nisheeth K. Vishnoi (Eds.), Vol. 24. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, 189--200.Google Scholar
- Pavel Pudlák. 2009. Quantum deduction rules. Ann. Pure Appl. Logic 157, 1 (2009), 16--29. Google ScholarCross Ref
- Omer Reingold. 2008. Undirected connectivity in log-space. J. ACM 55, 4, Article 17 (2008), 24 pages. (Originally appeared in STOC’05). Google ScholarDigital Library
- Nathan Segerlind. 2007. The complexity of propositional proofs. Bull. Symbol. Logic 13, 4 (2007), 417--481. Google ScholarCross Ref
- R. Szelepcsényi. 1988. The method of forced enumeration for nondeterministic automata. Acta Inform. 26, 3 (Nov. 1988), 279--284. DOI:http://dx.doi.org/10.1007/BF00299636 Google ScholarDigital Library
- Oswald Veblen. 1912. An application of modular equations in analysis situs. Ann. Math. 14, 1/4 (1912), 86--94. Google ScholarCross Ref
- H. Venkateswaran. 1991. Properties that characterize LOGCFL. J. Comput. System Sci. 43, 2 (1991), 380--404. DOI:http://dx.doi.org/10.1016/0022-0000(91)90020-6 Google ScholarDigital Library
Index Terms
Small Depth Proof Systems
Recommendations
Verifying proofs in constant depth
In this paper we initiate the study of proof systems where verification of proofs proceeds by NC0 circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages ...
On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
An exponential lower bound for the size of tree-like cutting planes refutations of a certain family of conjunctive normal form (CNF) formulas with polynomial size resolution refutations is proved. This implies an exponential separation between the tree-...
Parameterized Bounded-Depth Frege Is not Optimal
A general framework for parameterized proof complexity was introduced by Dantchev et al. [2007]. There, the authors show important results on tree-like Parameterized Resolution---a parameterized version of classical Resolution---and their gap complexity ...
Comments