La rédaction des argumentations et de preuves logiques n’est pas toujours facile. Une preuve ne doit pas seulement être exempte d’erreurs, elle doit aussi être compréhensible. Les systèmes de preuve interactifs aident à répondre à ces deux exigences. Indiquez vos hypothèses, formulez votre argumentation et guidez votre assistant numérique pas à pas vers une conclusion convaincante. Vous avez maintenant la certitude que votre argumentation a été comprise par le système de preuve, qu’elle a été rigoureusement vérifiée et qu’elle est correcte!

Nous apprenons, à l’aide du système de preuve 'Coq', comment les définitions et les preuves logiques peuvent être représentées de manière lisible et vérifiable aussi bien pour les personnes que pour les machines. L’outil peut, au choix, être installé localement ou être appelé directement dans un navigateur web. Le matériel pédagogique est en anglais, tandis que la langue d'enseignement peut être adaptée à l'anglais, au français ou à l'allemand en fonction des préférences des étudiants.