{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T12:05:21Z","timestamp":1773662721570,"version":"3.50.1"},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4394,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2002,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of <jats:italic>k<\/jats:italic> lines contains <jats:italic>n<\/jats:italic> cycles then there exists an acyclic proof with <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S002248120000983X_inline1\"\/>(<jats:italic>k<jats:sup>n+1<\/jats:sup><\/jats:italic>) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search.<\/jats:p>","DOI":"10.2178\/jsl\/1190150028","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T14:12:10Z","timestamp":1197555130000},"page":"35-60","source":"Crossref","is-referenced-by-count":4,"title":["The cost of a cycle is a square"],"prefix":"10.1017","volume":"67","author":[{"given":"A.","family":"Carbone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120000983X_ref022","first-page":"234","article-title":"Complexity of a derivation in the propositional calculus","volume":"8","author":"Tseitin","year":"1968","journal-title":"Zapiski Nauchnykh Seminarov, Leningrad Otdelenie Matematicheski\u012d Institut, Akademiya Nauka SSSR"},{"key":"S002248120000983X_ref017","volume-title":"Translations of Mathematical Monographs 128","author":"Orevkov","year":"1993"},{"key":"S002248120000983X_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BF01629444"},{"key":"S002248120000983X_ref013","volume-title":"Proof theory and logical complexity","volume":"1","author":"Girard","year":"1987"},{"key":"S002248120000983X_ref009","volume-title":"Mathematical monographs","author":"Carbone","year":"2000"},{"key":"S002248120000983X_ref007","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-99-02300-4"},{"key":"S002248120000983X_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00031-1"},{"key":"S002248120000983X_ref003","volume-title":"Personal communication","author":"Buss","year":"1993"},{"key":"S002248120000983X_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90059-U"},{"key":"S002248120000983X_ref008","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-97-00715-5"},{"key":"S002248120000983X_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S002248120000983X_ref010","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of propositional proof systems"},{"key":"S002248120000983X_ref019","first-page":"981","volume":"62","author":"Pudl\u00e1k","year":"1997","journal-title":"Lower bounds for resolution and cutting plane proofs and monotone computations"},{"key":"S002248120000983X_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S002248120000983X_ref021","volume-title":"Proof theory","author":"Takeuti","year":"1987"},{"key":"S002248120000983X_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF02391554"},{"key":"S002248120000983X_ref018","volume-title":"Handbook of proof theory","author":"Pudl\u00e1k","year":"1996"},{"key":"S002248120000983X_ref015","first-page":"457","volume":"62","author":"Kraj\u00ed\u010dek","year":"1997","journal-title":"Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic"},{"key":"S002248120000983X_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00019-X"},{"key":"S002248120000983X_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00009-3"},{"key":"S002248120000983X_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S002248120000983X_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(78)90011-6"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120000983X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T21:35:15Z","timestamp":1557178515000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120000983X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S002248120000983X"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150028","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}