Cirquent calculus

Cirquent calculus (circuit sequent calculus) is a proof calculus that combines aspects of sequent calculus and boolean circuits. Its proof-objects are graph-style objects, termed cirquents, as opposed to the traditional tree-style objects such as formulas or sequents. Cirquents come in a variety of forms, but they all share one main characteristic feature, making them different from the more traditional objects of syntactic manipulation. This feature is the ability to explicitly account for possible sharing of subcomponents between different components. The idea is that, just as in a Boolean circuit, the output of a gate can be reused arbitrarily often by subsequent gates, so in a cirquent proof, proven subformulas can be reused.

For instance, it is possible to write an expression where two subexpressions F and E, while neither one is a subexpression of the other, still have a common occurrence of a subexpression G (as opposed to having two different occurrences of G, one in F and one in E).