Editing Proof calculus (section)

==Examples of proof calculi==
The most widely known proof calculi are those classical calculi that are still in widespread use:
*The class of [[Hilbert system]]s,<ref name=":0" /> of which the most famous example is the 1928 [[Hilbert-Ackermann system|Hilbert–Ackermann system]] of [[first-order logic]];
*[[Gerhard Gentzen]]'s calculus of [[natural deduction]], which is the first formalism of [[structural proof theory]], and which is the cornerstone of the [[formulae-as-types correspondence]] relating logic to [[functional programming]];
*Gentzen's [[sequent calculus]], which is the most studied formalism of structural proof theory.

Many other proof calculi were, or might have been, seminal, but are not widely used today.

*[[Aristotle]]'s  [[syllogistic]] calculus, presented in the ''[[Organon]]'', readily admits formalisation. There is still some modern interest in [[syllogism]]s, carried out under the [[aegis]] of [[term logic]].
*[[Gottlob Frege]]'s two-dimensional notation of the ''[[Begriffsschrift]]'' (1879) is usually regarded as introducing the modern concept of [[Quantifier (logic)|quantifier]] to logic.
*[[Charles Sanders Peirce|C.S. Peirce]]'s [[existential graph]] easily might have been seminal, had history worked out differently.

Modern research in logic teems with rival proof calculi:
*Several systems have been proposed that replace the usual textual syntax with some graphical syntax. [[proof net]]s and [[cirquent calculus]] are among such systems.
*Recently, many logicians interested in [[structural proof theory]] have proposed calculi with [[deep inference]], for instance [[display logic]], [[hypersequent]]s, the [[calculus of structures]], and [[bunched implication]].