{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:12Z","timestamp":1750220052717,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,4,7]],"date-time":"2023-04-07T00:00:00Z","timestamp":1680825600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council"},{"name":"European Union\u2019s Horizon 2020 research and innovation programme","award":["ERC-2014-CoG 648276"],"award-info":[{"award-number":["ERC-2014-CoG 648276"]}]},{"name":"MINECO","award":["TIN2013-48031-C4-1-P"],"award-info":[{"award-number":["TIN2013-48031-C4-1-P"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,7,31]]},"abstract":"<jats:p>Proofs in propositional logic are typically presented as trees of derived formulas or, alternatively, as directed acyclic graphs of derived formulas. This distinction between tree-like vs. dag-like structure is particularly relevant when making quantitative considerations regarding, for example, proof size. Here we analyze a more general type of structural restriction for proofs in rule-based proof systems. In this definition, proofs are directed graphs of derived formulas in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs \u201ccircular\u201d. We show that, for all sets of standard inference rules with single or multiple conclusions, circular proofs are sound. We start the study of the proof complexity of circular proofs at Circular Resolution, the circular version of Resolution. We immediately see that Circular Resolution is stronger than dag-like Resolution since, as we show, the propositional encoding of the pigeonhole principle has circular Resolution proofs of polynomial size. Furthermore, for derivations of clauses from clauses, we show that Circular Resolution is, surprisingly, equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: (1) polynomial-time (LP-based) algorithms that find Circular Resolution proofs of constant width, (2) examples that separate Circular from dag-like Resolution, such as the pigeonhole principle and its variants, and (3) exponentially hard cases for Circular Resolution. Contrary to the case of Circular Resolution, for Frege we show that circular proofs can be converted into tree-like proofs with at most polynomial overhead.<\/jats:p>","DOI":"10.1145\/3579997","type":"journal-article","created":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T11:54:53Z","timestamp":1675079693000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Circular (Yet Sound) Proofs in Propositional Logic"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3732-1989","authenticated-orcid":false,"given":"Albert","family":"Atserias","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4003-3168","authenticated-orcid":false,"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[{"name":"Sapienza Universit\u00e0 di Roma, Roma, Italy"}]}],"member":"320","published-online":{"date-parts":[[2023,4,7]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21951"},{"key":"e_1_3_1_3_2","volume-title":"Proceedings of 34th Annual Conference on Computational Complexity (CCC\u201919)","volume":"137","author":"Atserias A.","year":"2019","unstructured":"A. Atserias and T. Hakoniemi. 2019. Size-degree trade-offs for sums-of-squares and positivstellensatz proofs. In Proceedings of 34th Annual Conference on Computational Complexity (CCC\u201919). Vol. 137, Schloss Dagstuhl - Leibniz Center for Informatics (LZI), 24:1\u201324:20."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_1"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2898435"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1137\/130950173"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.12204"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_13"},{"key":"e_1_3_1_11_2","volume-title":"Sequent Calculus Proof Systems for Inductive Definitions","author":"Brotherston J.","year":"2006","unstructured":"J. Brotherston. 2006. Sequent Calculus Proof Systems for Inductive Definitions. Ph.D. Dissertation. University of Edinburgh."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273826"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250790.1250837"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.01.002"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:1)2020"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_26"},{"key":"e_1_3_1_19_2","volume-title":"Puissance Expressive des Preuves Circulaires. (Expressive Power of Circular Proofs)","author":"Fortier J\u00e9r\u00f4me","year":"2014","unstructured":"J\u00e9r\u00f4me Fortier. 2014. Puissance Expressive des Preuves Circulaires. (Expressive Power of Circular Proofs). Ph.D. Dissertation. Aix-Marseille University, Aix-en-Provence, France. https:\/\/tel.archives-ouvertes.fr\/tel-01154972."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54487-9_59"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00157-2"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_11"},{"key":"e_1_3_1_24_2","volume-title":"Bounded Arithmetic, Propositional Logic, Complexity Theory","author":"Kraj\u00ed\u010dek J.","year":"1994","unstructured":"J. Kraj\u00ed\u010dek. 1994. Bounded Arithmetic, Propositional Logic, Complexity Theory. Cambridge."},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_16"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00136-0"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1137\/100816833"},{"key":"e_1_3_1_30_2","volume-title":"Combinatorial Optimization: Polyhedra and Efficiency","author":"Schrijver Alexander","year":"2003","unstructured":"Alexander Schrijver. 2003. Combinatorial Optimization: Polyhedra and Efficiency. Vol. 24. Springer Science & Business Media."},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020319000613"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1137\/0403036"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565687"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-008-9133-6"},{"key":"e_1_3_1_36_2","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/BFb0079691","volume-title":"The Syntax and Semantics of Infinitary Languages","author":"Tait W. W.","year":"1968","unstructured":"W. W. Tait. 1968. Normal derivability in classical logic. In The Syntax and Semantics of Infinitary Languages, J. Barwise (Ed.). Lecture Notes in Mathematics, Vol. 72. Springer-Verlag, 204\u2013236."},{"key":"e_1_3_1_37_2","author":"Vinyals M.","year":"2018","unstructured":"M. Vinyals. 2018. Personal communication. (2018).","journal-title":"Personal communication"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579997","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3579997","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:19Z","timestamp":1750183699000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579997"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,7]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,7,31]]}},"alternative-id":["10.1145\/3579997"],"URL":"https:\/\/doi.org\/10.1145\/3579997","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,4,7]]},"assertion":[{"value":"2019-09-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}