{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T05:25:40Z","timestamp":1672377940957},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,1]]},"abstract":"\n The Jordan curve theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory\n V<\/jats:bold>\n 0<\/jats:sup>\n (2) (corresponding to\n AC<\/jats:bold>\n 0<\/jats:sup>\n (2)) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory\n V<\/jats:bold>\n 0<\/jats:sup>\n (corresponding to\n AC<\/jats:bold>\n 0<\/jats:sup>\n ) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-connectivity tautologies have polynomial size\n AC<\/jats:bold>\n 0<\/jats:sup>\n (2)-\n Frege<\/jats:bold>\n -proofs, which improves results of Buss which only apply to the stronger proof system\n TC<\/jats:bold>\n 0<\/jats:sup>\n -\n Frege<\/jats:bold>\n .\n <\/jats:p>","DOI":"10.1145\/2071368.2071377","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-24","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The Complexity of Proving the Discrete Jordan Curve Theorem"],"prefix":"10.1145","volume":"13","author":[{"given":"Phuong","family":"Nguyen","sequence":"first","affiliation":[{"name":"McGill University"}]},{"given":"Stephen","family":"Cook","sequence":"additional","affiliation":[{"name":"University of Toronto"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21951"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.011"},{"key":"e_1_2_1_3_1","unstructured":"Cook S. 2005. Theories for complexity classes and their propositional translations. In Complexity of Computations and Proofs J. Kraji\u010dek Ed. 175--227. Cook S. 2005. Theories for complexity classes and their propositional translations. In Complexity of Computations and Proofs J. Kraji\u010dek Ed. 175--227."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Cook S. and Nguyen P. 2010. Logical Foundations of Proof Complexity. ASL Perspectives in Logic Series. Cambridge University Press. Cook S. and Nguyen P. 2010. Logical Foundations of Proof Complexity. ASL Perspectives in Logic Series. Cambridge University Press.","DOI":"10.1017\/CBO9780511676277"},{"key":"e_1_2_1_5_1","unstructured":"Cook S. and Rackoff C. 1997. Unpublished research notes. Cook S. and Rackoff C. 1997. Unpublished research notes."},{"key":"e_1_2_1_6_1","unstructured":"Hales T. 2005. A verified proof of the Jordan curve theorem. Seminar Talk Department of Mathematics University of Toronto. Hales T. 2005. A verified proof of the Jordan curve theorem. Seminar Talk Department of Mathematics University of Toronto."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.2007.11920481"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Immerman N. 1999. Descriptive Complexity. Springer. Immerman N. 1999. Descriptive Complexity . Springer.","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Kraji\u010dek J. 1995. Bounded Arithmetic Propositional Logic and Complexity Theory. Cambridge University Press. Kraji\u010dek J. 1995. Bounded Arithmetic Propositional Logic and Complexity Theory. Cambridge University Press.","DOI":"10.1017\/CBO9780511529948"},{"key":"e_1_2_1_10_1","unstructured":"Nguyen P. 2008. Bounded reverse mathematics. Ph.D. thesis University of Toronto. http:\/\/www.cs.toronto.edu\/-pnguyen\/. Nguyen P. 2008. Bounded reverse mathematics. Ph.D. thesis University of Toronto. http:\/\/www.cs.toronto.edu\/-pnguyen\/."},{"key":"e_1_2_1_11_1","first-page":"1","article-title":"Theory for TC0 and other small complexity classes","volume":"2","author":"Nguyen P.","year":"2005","journal-title":"Logical Meth. Comput. Sci."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.48"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Razborov A. A. 1995. Bounded arithmetic and lower bounds in Boolean complexity. In Feasible Mathematics II P. Clote and J. B. Remmel Eds. Birkhauser 344--386. Razborov A. A. 1995. Bounded arithmetic and lower bounds in Boolean complexity. In Feasible Mathematics II P. Clote and J. B. Remmel Eds. Birkhauser 344--386.","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Simpson S. 1999. Subsystems of Second-Order Arithmetic. Springer. Simpson S. 1999. Subsystems of Second-Order Arithmetic . Springer.","DOI":"10.1007\/978-3-642-59971-2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2324180"},{"key":"e_1_2_1_16_1","unstructured":"Urquhart A. 2001. Hex example. Email correspondence Toronto theory group. Urquhart A. 2001. Hex example. Email correspondence Toronto theory group."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275794"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071368.2071377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T18:15:35Z","timestamp":1672337735000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071368.2071377"],"URL":"http:\/\/dx.doi.org\/10.1145\/2071368.2071377","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2012,1]]},"assertion":[{"value":"2010-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}