### Abstract

This work formalizes soundness and completeness of a one-sided sequent
calculus for first-order logic. The completeness is shown via a
translation from a complete semantic tableau calculus, the proof of
which is based on the First-Order Logic According to Fitting theory.
The calculi and proof techniques are taken from Ben-Ari's
Mathematical Logic for Computer Science.

BSD License