{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T16:05:29Z","timestamp":1750694729699,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,10,21]],"date-time":"2016-10-21T00:00:00Z","timestamp":1477008000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2017,3,31]]},"abstract":"\n A proof system for a language\n L<\/jats:italic>\n is a function\n f<\/jats:italic>\n such that Range(\n f<\/jats:italic>\n ) is exactly\n L<\/jats:italic>\n . In this article, 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 proof systems that can be computed by bounded fanin circuits of constant depth (NC\n 0<\/jats:sup>\n ) or of\n O<\/jats:italic>\n (log\u2009log\u2009\n n<\/jats:italic>\n ) depth but with\n O<\/jats:italic>\n (1) alternations (poly log AC\n 0<\/jats:sup>\n ). 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.\n <\/jats:p>\n \n We identify exactly how much power we need for proof systems to capture all regular languages. We show that all regular languages have poly log AC\n 0<\/jats:sup>\n proof systems, and from a previous result (Beyersdorff et al. [2011a], where NC\n 0<\/jats:sup>\n proof systems were first introduced), this is tight. Our technique also shows that M\n aj<\/jats:sc>\n has poly log AC\n 0<\/jats:sup>\n proof system.\n <\/jats:p>\n \n We explore the question of whether T\n aut<\/jats:sc>\n has NC\n 0<\/jats:sup>\n proof systems. Addressing this question about 2TAUT, and since 2TAUT is closely related to reachability in graphs, we ask the same question about Reachability. We show that if Directed reachability has NC\n 0<\/jats:sup>\n proof systems, then so does 2TAUT. We then show that both Undirected Reachability and Directed UnReachability have NC\n 0<\/jats:sup>\n proof systems, but Directed Reachability is still open.\n <\/jats:p>\n \n In the context of how much power is needed for proof systems for languages in NP, we observe that proof systems for a good fraction of languages in NP do not need the full power of AC\n 0<\/jats:sup>\n ; they have SAC\n 0<\/jats:sup>\n or coSAC\n 0<\/jats:sup>\n proof systems.\n <\/jats:p>","DOI":"10.1145\/2956229","type":"journal-article","created":{"date-parts":[[2016,10,25]],"date-time":"2016-10-25T12:37:00Z","timestamp":1477399020000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Small Depth Proof Systems"],"prefix":"10.1145","volume":"9","author":[{"given":"Andreas","family":"Krebs","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nutan","family":"Limaye","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[{"name":"The Institute of Mathematical Sciences, Chennai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karteek","family":"Sreenivasaiah","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Informatics, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,10,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90037-8"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.63138"},{"volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Century","author":"Beame Paul","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90253-P"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2462896.2462898"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2034006.2034019"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.006"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218038"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1203350791"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645730.668189"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744431"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11753728_22"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/12130.12132"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13562-0_4"},{"volume":"5","volume-title":"Proceedings of the of 27th Annual Symposium on Theoretical Aspects of Computer Science (STACS) (LIPIcs)","author":"Edward","key":"e_1_2_1_17_1"},{"volume-title":"Ullman","year":"1979","author":"Hopcroft John E.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/0217058"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1972.1054893"},{"key":"e_1_2_1_21_1","volume-title":"Anil Seth and Nisheeth K. Vishnoi (Eds.)","volume":"24","author":"Krebs Andreas","year":"2013"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.09.017"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391291"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00299636"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/1967604"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(91)90020-6"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2956229","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2956229","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:43Z","timestamp":1750217983000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2956229"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,21]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3,31]]}},"alternative-id":["10.1145\/2956229"],"URL":"https:\/\/doi.org\/10.1145\/2956229","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2016,10,21]]},"assertion":[{"value":"2014-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-10-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}