{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:12:15Z","timestamp":1750306335511,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,7,5]],"date-time":"2016-07-05T00:00:00Z","timestamp":1467676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-14-CE25-0005"],"award-info":[{"award-number":["ANR-14-CE25-0005"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,7,5]]},"DOI":"10.1145\/2933575.2934570","type":"proceedings-article","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T13:34:47Z","timestamp":1476452087000},"page":"126-135","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["From positive and intuitionistic bounded arithmetic to monotone proof complexity"],"prefix":"10.1145","author":[{"given":"Anupam","family":"Das","sequence":"first","affiliation":[{"name":"LIP, Universit\u00e9 de Lyon, CNRS, ENS de Lyon, Universit\u00e9 Claude-Bernard Lyon, Milyon"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Monotone proofs of the pigeon hole principle. Electronic Colloquium on Computational Complexity (ECCC), 7(8)","author":"Atserias Albert","year":"2000","unstructured":"Albert Atserias , Nicola Galesi , and Ricard Gavald\u00e0 . Monotone proofs of the pigeon hole principle. Electronic Colloquium on Computational Complexity (ECCC), 7(8) , 2000 . Albert Atserias, Nicola Galesi, and Ricard Gavald\u00e0. Monotone proofs of the pigeon hole principle. Electronic Colloquium on Computational Complexity (ECCC), 7(8), 2000."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(02)00020-X"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1190150032"},{"issue":"3","key":"e_1_3_2_1_4_1","first-page":"575","article-title":"Monotone sequent calculus and resolution","volume":"42","author":"B\u00edlkov\u00e1 Marta","year":"2001","unstructured":"Marta B\u00edlkov\u00e1 . Monotone sequent calculus and resolution . Commentationes Mathematicae Universitatis Carolinae , 42 ( 3 ): 575 -- 582 , 2001 . Marta B\u00edlkov\u00e1. Monotone sequent calculus and resolution. Commentationes Mathematicae Universitatis Carolinae, 42(3):575--582, 2001.","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_7"},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45653-8_24","volume-title":"LPAR","author":"Br\u00fcnnler Kai","year":"2001","unstructured":"Kai Br\u00fcnnler and Alwen Fernanto Tiu . A local system for classical logic . In LPAR 2001 , volume 2250 of Lecture Notes in Computer Science , pages 347 -- 361 . Springer-Verlag , 2001. Kai Br\u00fcnnler and Alwen Fernanto Tiu. A local system for classical logic. In LPAR 2001, volume 2250 of Lecture Notes in Computer Science, pages 347--361. Springer-Verlag, 2001."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462186"},{"key":"e_1_3_2_1_8_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-642-17511-4_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '16)","author":"Bruscoli Paola","year":"2010","unstructured":"Paola Bruscoli , Alessio Guglielmi , Tom Gundersen , and Michel Parigot . A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae . In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '16) , volume 6355 of Lecture Notes in Computer Science , pages 136 -- 153 . Springer-Verlag , 2010 . Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '16), volume 6355 of Lecture Notes in Computer Science, pages 136--153. Springer-Verlag, 2010."},{"key":"e_1_3_2_1_9_1","series-title":"Studies in Proof Theory","volume-title":"Bounded arithmetic","author":"Buss Samuel R.","year":"1986","unstructured":"Samuel R. Buss . Bounded arithmetic , volume 1 of Studies in Proof Theory . Bibliopolis , Naples , 1986 . Samuel R. Buss. Bounded arithmetic, volume 1 of Studies in Proof Theory. Bibliopolis, Naples, 1986."},{"key":"e_1_3_2_1_10_1","first-page":"77","volume-title":"Proceedings of the Conference hold at the University of California","author":"Buss Samuel R.","year":"1986","unstructured":"Samuel R. Buss . The polynomial hierarchy and intuitionistic bounded arithmetic. In Structure in Complexity Theory , Proceedings of the Conference hold at the University of California , Berkeley, California , June 2-5, 1986 , pages 77 -- 103 , 1986. Samuel R. Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. In Structure in Complexity Theory, Proceedings of the Conference hold at the University of California, Berkeley, California, June 2-5, 1986, pages 77--103, 1986."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90059-U"},{"key":"e_1_3_2_1_12_1","volume-title":"Handbook of proof theory","author":"Buss Samuel R.","year":"1998","unstructured":"Samuel R. Buss , editor. Handbook of proof theory . Elsevier , Amsterdam , 1998 . Samuel R. Buss, editor. Handbook of proof theory. Elsevier, Amsterdam, 1998."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511676277","volume-title":"Logical Foundations of Proof Complexity","author":"Cook Stephen","year":"2010","unstructured":"Stephen Cook and Phuong Nguyen . Logical Foundations of Proof Complexity . Cambridge University Press , New York, NY, USA , 1 st edition, 2010 . Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, New York, NY, USA, 1st edition, 2010.","edition":"1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/73007.73017"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30870-3_15"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603164"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:4)2015"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of intuitionism","author":"Dummett Michael","year":"2000","unstructured":"Michael Dummett . Elements of intuitionism . Oxford University Press , 2000 . Michael Dummett. Elements of intuitionism. Oxford University Press, 2000."},{"key":"e_1_3_2_1_19_1","volume-title":"Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1:9):1--36","author":"Guglielmi Alessio","year":"2008","unstructured":"Alessio Guglielmi and Tom Gundersen . Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1:9):1--36 , 2008 . Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1:9):1--36, 2008."},{"key":"e_1_3_2_1_20_1","first-page":"135","volume-title":"21st International Conference on Rewriting Techniques and Applications (RTA '10), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs)","author":"Guglielmi Alessio","year":"2010","unstructured":"Alessio Guglielmi , Tom Gundersen , and Michel Parigot . A proof calculus which reduces syntactic bureaucracy. In Christopher Lynch, editor , 21st International Conference on Rewriting Techniques and Applications (RTA '10), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 135 -- 150 . Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik , 2010 . Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A proof calculus which reduces syntactic bureaucracy. In Christopher Lynch, editor, 21st International Conference on Rewriting Techniques and Applications (RTA '10), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 135--150. Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 2010."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275282"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn054"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.10.002"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201020071"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/225488"},{"key":"e_1_3_2_1_26_1","first-page":"19","volume-title":"Structures and Deduction","author":"McKinley Richard","year":"2005","unstructured":"Richard McKinley . Classical categories and deep inference . In Structures and Deduction , pages 19 -- 33 . Technische Universit\u00e4t Dresden , 2005 . ICALP Workshop. ISSN 1430-211X. Richard McKinley. Classical categories and deep inference. In Structures and Deduction, pages 19--33. Technische Universit\u00e4t Dresden, 2005. ICALP Workshop. ISSN 1430-211X."},{"key":"e_1_3_2_1_27_1","first-page":"237","volume-title":"W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, eds","author":"Paris J.B.","year":"1981","unstructured":"J.B. Paris and A.J. Wilkie . \u03940 sets and induction. Open Days in Model Theory and Set Theory , W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, eds , pages 237 -- 248 , 1981 . J.B. Paris and A.J. Wilkie. \u03940 sets and induction. Open Days in Model Theory and Set Theory, W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, eds, pages 237--248, 1981."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107325944.010"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2012.07.004"},{"key":"e_1_3_2_1_30_1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Proof Theory","author":"Takeuti Gaisi","year":"1975","unstructured":"Gaisi Takeuti . Proof Theory , volume 81 of Studies in Logic and the Foundations of Mathematics . North-Holland , 1975 . Gaisi Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1975."}],"event":{"name":"LICS '16: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"New York NY USA","acronym":"LICS '16"},"container-title":["Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/2933575.2934570","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2934570","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:53Z","timestamp":1750222493000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/2933575.2934570"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,5]]},"references-count":30,"alternative-id":["10.1145\/2933575.2934570","10.1145\/2933575"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/2933575.2934570","relation":{},"subject":[],"published":{"date-parts":[[2016,7,5]]},"assertion":[{"value":"2016-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}