{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:29:29Z","timestamp":1761611369609,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,3,25]],"date-time":"2015-03-25T00:00:00Z","timestamp":1427241600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Introduced in 2006 by Japaridze, cirquent calculus is a refinement of sequent\ncalculus. The advent of cirquent calculus arose from the need for a deductive\nsystem with a more explicit ability to reason about resources. Unlike the more\ntraditional proof-theoretic approaches that manipulate tree-like objects\n(formulas, sequents, etc.), cirquent calculus is based on circuit-style\nstructures called cirquents, in which different \"peer\" (sibling, cousin, etc.)\nsubstructures may share components. It is this resource sharing mechanism to\nwhich cirquent calculus owes its novelty (and its virtues). From its inception,\ncirquent calculus has been paired with an abstract resource semantics. This\nsemantics allows for reasoning about the interaction between a resource\nprovider and a resource user, where resources are understood in the their most\ngeneral and intuitive sense. Interpreting resources in a more restricted\ncomputational sense has made cirquent calculus instrumental in axiomatizing\nvarious fundamental fragments of Computability Logic, a formal theory of\n(interactive) computability. The so-called \"classical\" rules of cirquent\ncalculus, in the absence of the particularly troublesome contraction rule,\nproduce a sound and complete system CL5 for Computability Logic. In this paper,\nwe investigate the computational complexity of CL5, showing it is\n$\\Sigma_2^p$-complete. We also show that CL5 without the duplication rule has\npolynomial size proofs and is NP-complete.<\/jats:p>","DOI":"10.2168\/lmcs-11(1:12)2015","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:33:27Z","timestamp":1431934407000},"source":"Crossref","is-referenced-by-count":1,"title":["The Computational Complexity of Propositional Cirquent Calculus"],"prefix":"10.46298","volume":"Volume 11, Issue 1","author":[{"given":"Matthew Steven","family":"Bauer","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2015,3,25]]},"reference":[{"key":"961:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1127\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1127\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:04:14Z","timestamp":1681243454000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1127"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,25]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(1:12)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1401.1849","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1401.1849","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2015,3,25]]},"article-number":"1127"}}