ADG 2016
ADG 2016
Différences entre les versions de « Co-located event »
De ADG 2016
Ligne 4 : | Ligne 4 : | ||
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. | ||
− | + | ==Organizer:== Julien Narboux | |
− | + | ==Talks:== | |
− | + | === Tomas Recio (University of Cantabria) === | |
'''Title:''' "Computer assisted theorem proving for the education or Computer assisted education for theorem proving?”. | '''Title:''' "Computer assisted theorem proving for the education or Computer assisted education for theorem proving?”. | ||
Ligne 14 : | Ligne 14 : | ||
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. | 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 | '''Title:''' edukera : a point and click proof assistant for education | ||
Ligne 26 : | Ligne 26 : | ||
* student feedback (from experiment at UPMC university) | * 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:42
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)