sequent calculus

The term “sequent calculus” has two related meanings.

In the strict sense, the sequent calculus is, essentially, Gentzen's system LK; i.e., the calculus for the entailment relation that permits an arbitrary number of formulae on either side of the .