Cirquent calculus

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.

The approach was introduced by G. Japaridze[1] as an alternative proof theory capable of "taming" various nontrivial fragments of his computability logic, which had otherwise resisted all axiomatization attempts within the traditional proof-theoretic frameworks.

Unlike cirquent calculus, neither approach thus permits mixed cases where some identical subformulas are shared and some not.

Among the later-found applications of cirquent calculus was the use of it to define a semantics for purely propositional independence-friendly logic.

[6] Syntactically, cirquent calculi are deep inference systems with the unique feature of subformula-sharing.

Cirquents can be thought of as collections of sequents with possibly shared elements
Cirquent for the "two out of three" combination of resources, inexpressible in linear logic
Linear logic understands the displayed formula as the left cirquent, while classical logic as the right cirquent