Calculus of structures
Encyclopedia
The calculus of structures is a proof calculus
with deep inference
for studying the structural proof theory
of noncommutative logic
. The calculus has since been applied to study linear logic
, classical logic
, modal logic
, and process calculi, and many benefits are claimed to follow in these investigations from the way in which deep inference is made available in the calculus.
Proof calculus
In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules...
with deep inference
Deep inference
Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity...
for studying the structural proof theory
Structural proof theory
In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof.-Analytic proof:...
of noncommutative logic
Noncommutative logic
Noncommutative logic is an extension of linear logic which combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek calculus...
. The calculus has since been applied to study linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
, classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
, modal logic
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
, and process calculi, and many benefits are claimed to follow in these investigations from the way in which deep inference is made available in the calculus.
External links
- Calculus of structures homepage
- CoS in Maude: page documenting implementations of logical systems in the calculus of structures, using the Maude systemMaude systemThe Maude system is an implementation of rewriting logic developed at SRI International. It is similar in its general approach to Joseph Goguen's OBJ3 implementation of equational logic, but based on rewriting logic rather than order-sorted equational logic, and with a heavy emphasis on powerful...
.