  The sequent calculus is a formalism for proving validity of statements
formulated in First-Order Logic. It is routinely used in computer science
modules on mathematical logic. Formal proofs in the sequent calculus are finite
trees obtained by successively applying proof rules to formulas, thus
simplifying them step-by-step.
  Students often struggle with the mathematical formalities and the level of
abstraction that topics like formal logic and formal proofs involve. The
difficulties can be categorised as syntactic or semantic. On the syntactic
level, students need to understand what a correctly formed proof is, how rules
can be applied (on paper for instance) without leaving the mathematical
framework of the sequent calculus, and so on. Beyond this, on the semantic
level, students need to acquire strategies that let them find the right proof.
  The Sequent Calculus Trainer is a tool that is designed to aid students in
learning the techniques of proving given statements formally. In this paper we
describe the didactical motivation behind the tool and the techniques used to
address issues on the syntactic as well as on the semantic level.
