Skip to main content

Verifying Proofs in Constant Depth

  • Conference paper
Mathematical Foundations of Computer Science 2011 (MFCS 2011)

Abstract

In this paper we initiate the study of proof systems where verification of proofs proceeds by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages can be enumerated by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) functions. Our results show that the answer to this problem is not determined by the complexity of the language. On the one hand, we construct \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for a variety of languages ranging from regular to \(\protect{\ensuremath{\mathsf{NP}}}\)-complete. On the other hand, we show by combinatorial methods that even easy regular languages such as Exact-OR do not admit \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems. We also present a general construction of \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for regular languages with strongly connected NFA’s.

Research supported by a DAAD/DST grant, DFG grant VO 630/6-2, and by grant N. 20517 from the John Templeton Foundation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Agrawal, M.: The isomorphism conjecture for constant depth reductions. Journal of Computer and System Sciences 77(1), 3–13 (2010)

    Article  Google Scholar 

  2. Agrawal, M., Allender, E., Impagliazzo, R., Pitassi, T., Rudich, S.: Reducing the complexity of reductions. Computational Complexity 10(2), 117–138 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  3. Agrawal, M., Allender, E., Rudich, S.: Reductions in circuit complexity: An isomorphism theorem and a gap theorem. J. Comput. Syst. Sci. 57(2), 127–143 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  4. Applebaum, B., Ishai, Y., Kushilevitz, E.: Cryptography in NC0. SIAM J. Comput. 36(4), 845–888 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  5. Applebaum, B., Ishai, Y., Kushilevitz, E.: On pseudorandom generators with linear stretch in NC0. Computational Complexity 17(1), 38–69 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. Applebaum, B., Ishai, Y., Kushilevitz, E.: Cryptography with constant input locality. J. Cryptology 22(4), 429–469 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  7. Beyersdorff, O., Köbler, J., Müller, S.: Proof systems that take advice. Information and Computation 209(3), 320–332 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  8. Beyersdorff, O., Müller, S.: A tight Karp-Lipton collapse result in bounded arithmetic. ACM Transactions on Computational Logic 11(4) (2010)

    Google Scholar 

  9. Cook, S.A., Krajíček, J.: Consequences of the provability of NP ⊆ P/poly. The Journal of Symbolic Logic 72(4), 1353–1371 (2007)

    Article  MATH  Google Scholar 

  10. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44(1), 36–50 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  11. Cryan, M., Miltersen, P.B.: On pseudorandom generators in NC0. In: Proc. 26th Symposium on Mathematical Foundations of Computer Science, pp. 272–284 (2001)

    Google Scholar 

  12. Goldwasser, S., Gutfreund, D., Healy, A., Kaufman, T., Rothblum, G.N.: Verifying and decoding in constant depth. In: Proc.39th ACM Symposium on Theory of Computing, pp. 440–449 (2007)

    Google Scholar 

  13. Håstad, J.: One-way permutations in NC0. Inf. Process. Lett. 26(3), 153–155 (1987)

    Article  MATH  Google Scholar 

  14. Hirsch, E.A.: Optimal Acceptors and Optimal Proof Systems. In: Kratochvíl, J., Li, A., Fiala, J., Kolman, P. (eds.) TAMC 2010. LNCS, vol. 6108, pp. 28–39. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Hirsch, E.A., Itsykson, D.: Hirsch and Dmitry Itsykson. On optimal heuristic randomized semidecision procedures, with application to proof complexity. In: Proc. 27th Symposium on Theoretical Aspects of Computer Science, pp. 453–464 (2010)

    Google Scholar 

  16. Mossel, E., Shpilka, A., Trevisan, L.: On ε-biased generators in NC0. Random Struct. Algorithms 29(1), 56–81 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  17. Pudlák, P.: Quantum deduction rules. Annals of Pure and Applied Logic 157(1), 16–29 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  18. Segerlind, N.: The complexity of propositional proofs. Bulletin of Symbolic Logic 13(4), 417–481 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  19. Vollmer, H.: Introduction to Circuit Complexity – A Uniform Approach. Texts in Theoretical Computer Science. Springer, Heidelberg (1999)

    Google Scholar 

  20. Wegener, I.: The Complexity of Boolean Functions. Wiley-Teubner series in computer science. B. G. Teubner & John Wiley, Stuttgart (1987)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag GmbH Berlin Heidelberg

About this paper

Cite this paper

Beyersdorff, O. et al. (2011). Verifying Proofs in Constant Depth. In: Murlak, F., Sankowski, P. (eds) Mathematical Foundations of Computer Science 2011. MFCS 2011. Lecture Notes in Computer Science, vol 6907. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22993-0_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22993-0_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22992-3

  • Online ISBN: 978-3-642-22993-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics