The calculus of structures is a new proof theoretical formalism, introduced by Alessio Guglielmi in 1999. It exploits a new top-down symmetry of derivations made possible by deep inference. One can present deductive systems in the calculus of structures and analyse their properties, as one does in the sequent calculus, natural deduction and proof nets. Typical properties of interest are normalisation and cut elimination. The main purpose of this new formalism is to allow a richer combinatorial analysis of proofs than the other formalisms do.

Deep inference

Being one of the central concepts in the calculus of structures,
deep inference means deducing inside a formula, or structure, at any depth. Sequent calculus rules only see the root of formulae, what is called "shallow inference"; rules in the calculus of structures, instead, can rewrite at any position in the formula tree.

External sources

Deep Inference and the Calculus of Structures. The main web source on the subject. Maintained by A.Guglielmi.