Sequent calculus

In proof theory and mathematical logic, the sequent calculus is a widely known proof calculus for first-order logic (and propositional logic as a special case of it). The term "sequent calculus" applies both to a family of formal systems sharing a certain style of formal inference, and to its individual members, of which the first, and best known, is known under the name LK, distinguishing it from other systems in the family, such as LJ. Another term for such systems in general is Gentzen systems.

The sequent calculus LK was introduced by Gerhard Gentzen as a tool for studying natural deduction in 1934. It has turned out to be a very useful calculus for constructing logical derivations. The name itself is derived from the German term Logischer Kalkül, meaning "logical calculus." Sequent calculi and the general concepts relating to them are used widely in the whole field of proof theory and mathematical logic.

Reference:
http://en.wikipedia.org/wiki/Sequent_calculus