We describe our experience of using PhoX (the prover of C Raffalli) with undergraduate students in mathematic (in third year) to help them to do correct proofs. They proved, among other things, Heine's theorem.
Publié le : 2004-01-01
Classification:
proof assistant,
teaching mathematics,
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO],
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
@article{hal-00384656,
author = {David, Ren\'e and Raffalli, Christophe},
title = {An experiment concerning mathematical proofs on computers with French undergraduate students},
journal = {HAL},
volume = {2004},
number = {0},
year = {2004},
language = {en},
url = {http://dml.mathdoc.fr/item/hal-00384656}
}
David, René; Raffalli, Christophe. An experiment concerning mathematical proofs on computers with French undergraduate students. HAL, Tome 2004 (2004) no. 0, . http://gdmltest.u-ga.fr/item/hal-00384656/