Calculus of structures: Difference between revisions
Jump to navigation
Jump to search
No edit summary |
imported>Dexbot m Bot: Aligning section names with MOS:SECTIONS |
||
| Line 1: | Line 1: | ||
In [[mathematical logic]], 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. | In [[mathematical logic]], the '''calculus of structures''' is a [[proof calculus]] with [[deep inference]]<ref name=":0">{{Cite journal |last=Novaković |first=Novak |last2=Straßburger |first2=Lutz |date=2015-04-21 |title=On the Power of Substitution in the Calculus of Structures |url=https://doi.org/10.1145/2701424 |journal=ACM Trans. Comput. Logic |volume=16 |issue=3 |pages=19:1–19:20 |doi=10.1145/2701424 |issn=1529-3785|url-access=subscription }}</ref> 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. | ||
It was first introduced in 2001 in the paper ''A System of Interaction and Structure'' by Alessio Guglielmo of the [[University of Bath]].<ref name=":0" /> | |||
==References== | ==References== | ||
{{refs}} | {{refs}} | ||
== Further reading == | |||
* Alessio Guglielmi (2004)., 'A System of Interaction and Structure'. [[ACM Transactions on Computational Logic]]. | * 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. | * Kai Brünnler (2004). ''Deep Inference and Symmetry in Classical Proofs''. Logos Verlag. | ||
Latest revision as of 01:45, 4 November 2025
In mathematical logic, the calculus of structures is a proof calculus with deep inference[1] 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.
It was first introduced in 2001 in the paper A System of Interaction and Structure by Alessio Guglielmo of the University of Bath.[1]
References
<templatestyles src="Reflist/styles.css" />
Script error: No such module "Check for unknown parameters".
Further reading
- 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
- CoS in Maude: page documenting implementations of logical systems in the calculus of structures, using the Maude system.