IMPROOF

Nous cherchons à trouver des mécanismes universels pour le développement de preuves interactives qui sont basés sur la manipulation directe. L'objectif est d'utiliser des dispositifs d'entrée utilisateur riches tels que des souris, des écrans (multi-)tactiles, des écrans graphiques 3D, de réalité virtuelle, etc. et d'exploiter la grande variété d'actions interactives qu'ils permettent pour rendre la preuve interactive de théorèmes plus facile pour les novices et plus puissante pour les experts. Le projet se concentre à la fois sur les aspects fondamentaux de la démonstration interactive de théorèmes par manipulation directe, en élargissant son applicabilité aux systèmes déductifs généraux, et également sur des prototypes pratiques agnostiques qui peuvent supporter des interactions utilisateur riches indépendantes des interfaces textuelles.