Verifying Proofs in Constant Depth

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.

Authors

• Olaf Beyersdorff
• Samir Datta
• Meena Mahajan
• Gido Scharfenberger-Fabian
• Karteek Sreenivasaiah
• Michael Thomas 0001
• Heribert Vollmer

Keywords

No keywords are indexed for this paper.