  We present the Sequent Calculus Trainer, a tool that supports students in
learning how to correctly construct proofs in the sequent calculus for
first-order logic with equality. It is a proof assistant fostering the
understanding of all the syntactic principles that need to be obeyed in
constructing correct proofs. It does not provide any help in finding good proof
strategies. Instead it aims at understanding the sequent calculus on a lower
syntactic level that needs to be mastered before one can consider proof
strategies. Its main feature is a proper feedback system embedded in a
graphical user interface. We also report on some empirical findings that
indicate how the Sequent Calculus Trainer can improve the students' success in
learning sequent calculus for full first-order logic.
