Small Depth Proof Systems

Abstract. A proof system for a language L is a function f such that Range(f) is exactly L. In this paper, 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: they can be computed by bounded fanin circuits of constant depth (NC0), or of O(log logn) depth but with O(1) alternations (poly log AC0). Each out-put bit depends on very few input bits; thus such proof systems corre-spond 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 language have poly log AC0 proof systems, and from a previous result (Beyersdorff et al, MFCS 2011, where NC0 proof systems were first introduced), this is tight. Our tech-nique also shows that Maj has poly log AC0 proof system. We explore the question of whether Taut has NC0 proof systems. Ad-dressing this question about 2TAUT, and since 2TAUT is closely related to reachability in graphs, we ask the same question about Reachability. We show that both Undirected Reachability and Directed UnReachabil-ity have NC0 proof systems, but Directed Reachability is still open. In the context of how much power is needed for proof systems for lan-guages in NP, we observe that proof systems for a good fraction of lan-guages in NP do not need the full power of AC0; they have SAC0 or coSAC0 proof systems.