Writing arguments and logical proofs can be challenging. A proof must not only be error-free, but also be comprehensible. Interactive proof systems help to meet both these requirements.

State your hypotheses, formulate your arguments, and guide your digital assistant step by step towards a convincing conclusion. You now have the certainty that your argument has been understood and rigorously checked by the proof system and can thus assume that it is correct!

With the help of the 'Coq' proof system, we learn how logical definitions and proofs can be represented in a way that is legible and verifiable for both humans and computers. The tool can either be installed locally or accessed directly through a web browser. While the course material is in English, the teaching language can be adjusted to English, French or German according to students' preferences.