Subject: RE: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-14 20:35:04 GMT (34 weeks, 2 days, 6 hours and 10 minutes ago)
Woops, my apologies for multiple postings. Something funny is going on: posted (unsuccessfully) 4 days ago, appeared only now. Giorgi Japaridze http://www.csc.villanova.edu/~japaridz/ ________________________________________ From: owner-frogs@... [owner-frogs@...sden.de] On Behalf Of Giorgi Japaridze [giorgi.japaridze@...] Sent: Tuesday, September 11, 2007 2:48 AM To: Frogs@... Subject: [Frogs] Deep cirquent calculus Dear all, Just to advertise the following paper: Giorgi Japaridze Cirquent Calculus Deepened Full text available at http://arxiv.org/abs/0709.1308 A kind of marriage between (the earlier version of) cirquent calculus and CoS. Comments welcome. ABSTRACT. Cirquent calculus is a new proof-theoretic framework, whose main distinguishing feature is sharing: unlike the more traditional frameworks that manipulate tree- or forest-like objects such as formulas (Frege), sequents (Gentzen), hypersequents (Avron, Pottinger) or structures (Guglielmi), cirquent calculus deals with circuit-style constructs called cirquents, in which children may be shared between different parent nodes. Among its advantages are greater efficiency, flexibility and expressiveness. The approach was born in "Introduction to cirquent calculus and abstract resource semantics" (Journal of Logic and Computation, v.16). That so far the only paper on the subject introduced cirquent calculus in a special, "shallow" form, where the depths of cirquents were limited to two. While the shallow version of cirquent calculus was sufficient to achieve the main goal of that paper --- taming the otherwise wild class of binary tautologies and their instances --- the paper also outlined the possibility and expediency of studying more general, deep versions of cirquent calculi. The present article contains a realization of that outline. It elaborates a deep cirquent calculus system CL8 for classical propositional logic and the corresponding fragment of the resource-conscious computability logic. It also shows the existence of polynomial-size analytic CL8-proofs of the pigeonhole principle --- the family of tautologies known to have no such proofs in traditional systems.