ADG 2016
ADG 2016
Différences entre les versions de « Co-located event »
De ADG 2016
| Ligne 1 : | Ligne 1 : | ||
= Computer Assisted Theorem Proving for the Education = | = Computer Assisted Theorem Proving for the Education = | ||
| − | + | June 30, 2016, Stasbourg | |
The goal of this session is to bring together specialists of interactive and automatic theorem proving and specialists of mathematics education. | The goal of this session is to bring together specialists of interactive and automatic theorem proving and specialists of mathematics education. | ||
| Ligne 6 : | Ligne 6 : | ||
'''Organizer:''' Julien Narboux | '''Organizer:''' Julien Narboux | ||
| − | Confirmed participants: | + | ===Talks:=== |
| + | |||
| + | ==== Tomas Recio (University of Cantabria) ==== | ||
| + | '''Title:''' "Computer assisted theorem proving for the education or Computer assisted education for theorem proving?”. | ||
| + | |||
| + | '''Abstract:''' | ||
| + | The talk will be dual, in the sense of addressing the same issue from two different perspectives. One, in which the goals of mathematics education are a priori settled and computer assisted theorem proving is considered as a medium to achieve the given goals. Another one, where the goals of mathematics education should be reconsidered in view of the popularization of automated theorem proving features in dynamic geometry programs. | ||
| + | |||
| + | * Benoit Rognier ([http://edukera.com edukera.com]) | ||
| + | |||
| + | '''Title:''' edukera : a point and click proof assistant for education | ||
| + | |||
| + | '''Abstract:''' With edukera, students can now build mathematical proofs by selecting appropriate theorems among the list of authorized/available theorems. | ||
| + | |||
| + | The presentation covers : | ||
| + | * proof development interface (natural deduction style, scopes, backward/forward modes) | ||
| + | * theory design for educational purposes | ||
| + | * coq engine add-ons (paper management, term rewriting under lambdas) | ||
| + | * student feedback (from experiment at UPMC university) | ||
| + | |||
| + | ===Confirmed participants:=== | ||
* Vincent Pavan (University of Provence) | * Vincent Pavan (University of Provence) | ||
| − | |||
| − | |||
Version du 27 mars 2016 à 15:41
Computer Assisted Theorem Proving for the Education
June 30, 2016, Stasbourg
The goal of this session is to bring together specialists of interactive and automatic theorem proving and specialists of mathematics education.
Organizer: Julien Narboux
Talks:
Tomas Recio (University of Cantabria)
Title: "Computer assisted theorem proving for the education or Computer assisted education for theorem proving?”.
Abstract: The talk will be dual, in the sense of addressing the same issue from two different perspectives. One, in which the goals of mathematics education are a priori settled and computer assisted theorem proving is considered as a medium to achieve the given goals. Another one, where the goals of mathematics education should be reconsidered in view of the popularization of automated theorem proving features in dynamic geometry programs.
- Benoit Rognier (edukera.com)
Title: edukera : a point and click proof assistant for education
Abstract: With edukera, students can now build mathematical proofs by selecting appropriate theorems among the list of authorized/available theorems.
The presentation covers :
- proof development interface (natural deduction style, scopes, backward/forward modes)
- theory design for educational purposes
- coq engine add-ons (paper management, term rewriting under lambdas)
- student feedback (from experiment at UPMC university)
Confirmed participants:
- Vincent Pavan (University of Provence)
