Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis
| Autor: | Evmorfia Bartzia, Antoine Meyer, Julien Narboux |
|---|---|
| Přispěvatelé: | Institut Montpelliérain Alexander Grothendieck (IMAG), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), Laboratoire d'Informatique Gaspard-Monge (LIGM), École des Ponts ParisTech (ENPC)-Centre National de la Recherche Scientifique (CNRS)-Université Gustave Eiffel, Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Reinhard Hochmuth, María Trigueros, Narboux, Julien |
| Předmět: |
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
[INFO.INFO-MS] Computer Science [cs]/Mathematical Software [cs.MS] Transition to across and from university mathematics Teaching and learning of logic [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-IA]Computer Science [cs]/Computer Aided Engineering Novel approaches to teaching [INFO.INFO-IA] Computer Science [cs]/Computer Aided Engineering reasoning and proof Digital and other resources in university mathematics education Computer assisted theorem proving [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS] |
| Zdroj: | HAL INDRUM 2022: Fourth conference of the International Network for Didactic Research in University Mathematics INDRUM 2022: Fourth conference of the International Network for Didactic Research in University Mathematics, Reinhard Hochmuth, Oct 2022, Hanovre, Germany |
| Popis: | International audience; This paper presents an a-priori analysis of the use of five different interactive proof assistants for education, based on the resolution of a typical undergraduate exercise on abstract functions. It proposes to analyse these tools according to three main categories of aspects: language and interaction mode, automation and user assistance, and proof structure and visualisation. We argue that this analysis may help formulate and clarify further research questions on the possible impact of such tools on the development of reasoning and proving skills. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|