In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, 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:
* Formal language: The set ''L'' of formulas admitted by the system, for example, propositional logic or fir ...
with
deep inference for studying the
structural proof theory of
noncommutative logic. The calculus has since been applied to study
linear logic
Linear logic is a substructural logic proposed by French logician 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 ...
,
classical logic
Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this c ...
,
modal logic
Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields
it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...
, 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
ACM or A.C.M. may refer to:
Aviation
* AGM-129 ACM, 1990–2012 USAF cruise missile
* Air chief marshal
* Air combat manoeuvring or dogfighting
* Air cycle machine
* IATA airport code for Arica Airport in Amazonas Department, Colombia
Comput ...
.
* 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 and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
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