Deep cirquent calculus

Dear all,

Just to announce 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.