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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agrawal, M.: The isomorphism conjecture for constant depth reductions. Journal of Computer and System Sciences 77(1), 3–13 (2010)
Agrawal, M., Allender, E., Impagliazzo, R., Pitassi, T., Rudich, S.: Reducing the complexity of reductions. Computational Complexity 10(2), 117–138 (2001)
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)
Applebaum, B., Ishai, Y., Kushilevitz, E.: Cryptography in NC0. SIAM J. Comput. 36(4), 845–888 (2006)
Applebaum, B., Ishai, Y., Kushilevitz, E.: On pseudorandom generators with linear stretch in NC0. Computational Complexity 17(1), 38–69 (2008)
Applebaum, B., Ishai, Y., Kushilevitz, E.: Cryptography with constant input locality. J. Cryptology 22(4), 429–469 (2009)
Beyersdorff, O., Köbler, J., Müller, S.: Proof systems that take advice. Information and Computation 209(3), 320–332 (2011)
Beyersdorff, O., Müller, S.: A tight Karp-Lipton collapse result in bounded arithmetic. ACM Transactions on Computational Logic 11(4) (2010)
Cook, S.A., Krajíček, J.: Consequences of the provability of NP ⊆ P/poly. The Journal of Symbolic Logic 72(4), 1353–1371 (2007)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44(1), 36–50 (1979)
Cryan, M., Miltersen, P.B.: On pseudorandom generators in NC0. In: Proc. 26th Symposium on Mathematical Foundations of Computer Science, pp. 272–284 (2001)
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)
Håstad, J.: One-way permutations in NC0. Inf. Process. Lett. 26(3), 153–155 (1987)
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)
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)
Mossel, E., Shpilka, A., Trevisan, L.: On ε-biased generators in NC0. Random Struct. Algorithms 29(1), 56–81 (2006)
Pudlák, P.: Quantum deduction rules. Annals of Pure and Applied Logic 157(1), 16–29 (2009)
Segerlind, N.: The complexity of propositional proofs. Bulletin of Symbolic Logic 13(4), 417–481 (2007)
Vollmer, H.: Introduction to Circuit Complexity – A Uniform Approach. Texts in Theoretical Computer Science. Springer, Heidelberg (1999)
Wegener, I.: The Complexity of Boolean Functions. Wiley-Teubner series in computer science. B. G. Teubner & John Wiley, Stuttgart (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)