The calculus of structures is a
proof calculus In mathematical logic, a proof calculus or a proof system is built to prove statements.
Overview
A proof system includes the components:
* Language: The set ''L'' of formulas admitted by the system, for example, propositional logic or first-order ...
with
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. The term ''deep infer ...
for studying the
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, a kind of proof whose semantic properties are exposed. When all the theorems of a logic formal ...
of
noncommutative logic. The calculus has since been applied to study
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. Although the logic has also ...
,
classical logic,
modal logic, and
process calculi
In computer science, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and ...
, and many benefits are claimed to follow in these investigations from the way in which deep inference is made available in the calculus.
References
* Alessio Guglielmi (2004)., 'A System of Interaction and Structure'.
ACM Transactions on Computational Logic.
* Kai Brünnler (2004). ''Deep Inference and Symmetry in Classical Proofs''. Logos Verlag.
External links
Calculus of structures homepage page documenting implementations of
logical system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A for ...
s in the calculus of structures, using the
Maude system
The Maude system is an implementation of rewriting logic. 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 heav ...
.
Logical calculi
{{logic-stub