skip to main content
research-article

Small Depth Proof Systems

Published:21 October 2016Publication History
Skip Abstract Section

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.

References

  1. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  4. F. Bedard, F. Lemieux, and P. McKenzie. 1993. Extensions to Barrington’s M-program model. Theor. Comput. Sci. 107 (1993), 31--61. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  6. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  7. Olaf Beyersdorff, Johannes Köbler, and Sebastian Müller. 2011b. Proof systems that take advice. Inform. Comput. 209, 3 (2011), 320--332. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  10. 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 ScholarGoogle ScholarCross RefCross Ref
  11. Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (1979), 36--50. Google ScholarGoogle ScholarCross RefCross Ref
  12. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  13. 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 ScholarGoogle ScholarCross RefCross Ref
  14. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  15. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. 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 ScholarGoogle Scholar
  18. John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  21. 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 ScholarGoogle Scholar
  22. Pavel Pudlák. 2009. Quantum deduction rules. Ann. Pure Appl. Logic 157, 1 (2009), 16--29. Google ScholarGoogle ScholarCross RefCross Ref
  23. Omer Reingold. 2008. Undirected connectivity in log-space. J. ACM 55, 4, Article 17 (2008), 24 pages. (Originally appeared in STOC’05). Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Nathan Segerlind. 2007. The complexity of propositional proofs. Bull. Symbol. Logic 13, 4 (2007), 417--481. Google ScholarGoogle ScholarCross RefCross Ref
  25. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  26. Oswald Veblen. 1912. An application of modular equations in analysis situs. Ann. Math. 14, 1/4 (1912), 86--94. Google ScholarGoogle ScholarCross RefCross Ref
  27. 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 ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Small Depth Proof Systems

            Recommendations

            Comments

            Login options

            Check if you have access through your login credentials or your institution to get full access on this article.

            Sign in

            Full Access

            • Published in

              cover image ACM Transactions on Computation Theory
              ACM Transactions on Computation Theory  Volume 9, Issue 1
              March 2017
              118 pages
              ISSN:1942-3454
              EISSN:1942-3462
              DOI:10.1145/3007903
              Issue’s Table of Contents

              Copyright © 2016 ACM

              Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

              Publisher

              Association for Computing Machinery

              New York, NY, United States

              Publication History

              • Published: 21 October 2016
              • Accepted: 1 June 2016
              • Revised: 1 February 2016
              • Received: 1 September 2014
              Published in toct Volume 9, Issue 1

              Permissions

              Request permissions about this article.

              Request Permissions

              Check for updates

              Qualifiers

              • research-article
              • Research
              • Refereed
            • Article Metrics

              • Downloads (Last 12 months)6
              • Downloads (Last 6 weeks)1

              Other Metrics

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader