# 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:

${A}_{1}^{},{A}_{2}^{},\mathrm{...}{A}_{n}^{}\u22a2{B}_{1}^{},{B}_{2}^{},\mathrm{...}{B}_{m}^{}$

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:

$\Gamma \u22a2\Theta ,P,Q$

$\overline{\underset{}{\Gamma \u22a2\Theta ,P\vee Q}}$

### References:

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

### Comments:

No comments.