Subject: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-11 15:11:19 GMT (34 weeks, 5 days, 12 hours and 55 minutes ago)
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.