Small Depth Proof Systems
Andreas Krebs, Nutan Limaye, Meena Mahajan, Karteek Sreenivasaiah

TL;DR
This paper investigates highly restricted proof systems with small-depth circuits, characterizing their power to represent regular languages and related problems, and exploring their implications for NP and graph reachability.
Contribution
It precisely characterizes the computational power needed for proof systems to capture all regular languages using small-depth circuits and explores their application to NP and graph problems.
Findings
All regular languages have polylogarithmic AC^0 proof systems.
Undirected Reachability and UnReachability have NC^0 proof systems.
MAJ has a polylog AC^0 proof system.
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 proofsystems 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 (NC^0), or of O(log log n) depth but with O(1) alternations (polylog AC^0). Each output bit depends on very few input bits; thus such proof systems correspond 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 polylog AC^0 proof systems, and from a previous result (Beyersdorff et al, MFCS 2011, where NC^0 proof systems were first introduced), this is tight. Our technique also shows that MAJ has polylog AC^0 proof system. We…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
