# Catalogue of Artificial Intelligence Techniques

View Maths as: Images | MathML

## Sequent Calculus

### Categories: Inference and Reasoning

Author(s): Alan Smaill

A method of presenting a logic invented by Gentzen in which statements are made in the form:

where the sequent sign `$⊢$ ' indicates that given all the propositions ${A}_{i}^{}$

one of the propositions ${B}_{j}^{}$ holds. A logic is characterised by giving basic sequents as axioms and then allowing further sequents to be derived using rules of inference, typically associated with the introduction and elimination of the logical symbols of the language on either side of the arrow; for example, the rule for introducing a disjunction is:

where $\Gamma$ and $\Theta$ represent an arbitrary number of propositions. One of the advantages of sequent calculus over, say, Natural Deduction is the ease with which proofs can be manipulated (e.g., Gentzen's work on proof theory).

### References:

• Gallier, J.H., Logic for computer science: foundations of automatic theorem proving , Harper & Row, New York and London, 1986.