Informatics in Education

Students of proof theory, a branch of formal logic, can benefit from computerized tools. We describe the principles behind one such tool called ProEd. This tool is targeted especially at novice students, and therefore it is designed to support effortless exploratory use. We moreover argue that focusing on root-first proof construction in Sequent proof systems helps attain this effortlessness.