Introduction to Cirquent Calculus and Abstract Resource Semantics Export

@misc{citeulike:239665, abstract = {This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does. A need in substantially new deductive tools came with the advent of computability logic (see <A HREF="http://www.cis.upenn.edu/\~{}giorgi/cl.html">this http URL</A>) - the semantically constructed formal theory of computational resources, which has stubbornly resisted any axiomatization attempts within the framework of traditional syntactic approaches. Cirquent calculus breaks the ice. Removing contraction from the full collection of its rules yields a sound and complete system for the basic fragment CL5 of computability logic. Doing the same in sequent calculus, on the other hand, throws out the baby with the bath water, resulting in the strictly weaker affine logic. An implied claim of computability logic is that it is CL5 rather than affine logic that adequately materializes the resource philosophy traditionally associated with the latter. To strengthen this claim, the paper further introduces an abstract resource semantics and shows the soundness and completeness of CL5 with respect to it.}, archivePrefix = {arXiv}, author = {Japaridze, Giorgi}, citeulike-article-id = {239665}, citeulike-linkout-0 = {http://arxiv.org/abs/math.LO/0506553}, citeulike-linkout-1 = {http://arxiv.org/pdf/math.LO/0506553}, day = {27}, eprint = {math.LO/0506553}, keywords = {calculus, computability, logic, pnc, proof, sequent, structure}, month = {Jun}, posted-at = {2005-06-29 02:41:28}, priority = {2}, title = {Introduction to Cirquent Calculus and Abstract Resource Semantics}, url = {http://arxiv.org/abs/math.LO/0506553}, year = {2005} }

TY - ELEC ID - citeulike:239665 L3 - citeulike-article-id:239665 N2 - This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does. A need in substantially new deductive tools came with the advent of computability logic (see <A HREF="http://www.cis.upenn.edu/~giorgi/cl.html">this http URL</A>) - the semantically constructed formal theory of computational resources, which has stubbornly resisted any axiomatization attempts within the framework of traditional syntactic approaches. Cirquent calculus breaks the ice. Removing contraction from the full collection of its rules yields a sound and complete system for the basic fragment CL5 of computability logic. Doing the same in sequent calculus, on the other hand, throws out the baby with the bath water, resulting in the strictly weaker affine logic. An implied claim of computability logic is that it is CL5 rather than affine logic that adequately materializes the resource philosophy traditionally associated with the latter. To strengthen this claim, the paper further introduces an abstract resource semantics and shows the soundness and completeness of CL5 with respect to it. TI - Introduction to Cirquent Calculus and Abstract Resource Semantics KW - calculus KW - computability KW - logic KW - pnc KW - proof KW - sequent KW - structure AU - Japaridze, Giorgi PY - 2005/Jun/27/ UR - http://arxiv.org/abs/math.LO/0506553 ER -