proceeding Papers True Concurrency of Deep Inference Proofs


We give an event structures based true-concurrency characterization of deep inference proofs. The method is general to all deep inference systems that can be expressed as term rewriting systems. This delivers three consequences in a spectrum from theoretical to practical: the event structure characterization (i) provides a qualification of proof identity akin to proof nets for multiplicative linear logic and to atomic flows for classical logic; (ii) provides a concurrency theoretic interpretation for applications in logic programming; (iii) reduces the length of the proofs, and thereby extends the margin of proof search applications.

Paper Details