Paper Info
Title
Verifying proofs in constant depth
Abstract
In this paper we initiate the study of proof systems where verification of proofs proceeds by \protectNC0\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 \protectNC0\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 \protectNC0\protect{\ensuremath{\mathsf{NC}}}^{0} proof systems for a variety of languages ranging from regular to \protectNP\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 \protectNC0\protect{\ensuremath{\mathsf{NC}}}^{0} proof systems. We also present a general construction of \protectNC0\protect{\ensuremath{\mathsf{NC}}}^{0} proof systems for regular languages with strongly connected NFA’s.
Year
DOI
Venue
2011
10.1007/978-3-642-22993-0_11
ACM Transactions on Computation Theory
Keywords
Field
DocType
easy regular language,general construction,combinatorial method,verifying proof,nc0 proof system,proofs proceed,restricted model,constant depth,proof system,regular language,nc0 function,nc0 circuit
Analytic proof,Discrete mathematics,Combinatorics,Computer science,Abstract family of languages,Structural proof theory,Mathematical proof,Combinatorial proof,Cone (formal languages),Proof complexity,Pumping lemma for regular languages
Conference
Volume
ISSN
Citations 
6907
0302-9743
1
PageRank 
References 
Authors
0.37
20
7
Name
Order
Citations
PageRank
Olaf Beyersdorff122330.33
Samir Datta220019.82
Meena Mahajan368856.90
Gido Scharfenberger-Fabian421.44
Karteek Sreenivasaiah5135.30
Michael Thomas610.37
Heribert Vollmer780571.64