ADG 2010 - Munich
ADG 2010 - Munich
Différences entre les versions de « Schedule »
De ADG 2010 - Munich
| Ligne 1 : | Ligne 1 : | ||
<center><big><big><big>Thursday, July 22</big></big></big></center> | <center><big><big><big>Thursday, July 22</big></big></big></center> | ||
| − | + | 9h-9h45 '''Registration''' | |
| + | ---- | ||
| + | 9h45-10h '''Welcome'''<br> | ||
| + | 10h-11h '''Invited Talk'''<br> | ||
| + | '''Robert Joan-Arynio''': | ||
| + | ---- | ||
| + | 11h-11h20 '''Coffee break''' | ||
| + | ---- | ||
| + | 11h20-12h30 <big><big>session 1</big></big><br> | ||
| + | 11h20-11h50 '''Xiaoyu Chen''': Formal representation and Automated transformation of geometric statements <br> | ||
| + | 11h55-12h25 '''Pedro Quaresma''': TGTP - Thousands of geometric problems for geometric theorems provers | ||
| + | ------------ | ||
| + | <br> | ||
| + | 12h30-14h '''Lunch''' | ||
| + | <br> | ||
| + | ------------- | ||
| + | 14h-15h10 <big><big>session 2</big></big><br> | ||
| + | 14h-14h30 '''Phil Scott and Jacques Fleuriot:'''Idle time discovery in geometry theorem proving <br> | ||
| + | 14h35-15h05 '''Jean Duprat''': The Euclid's plane: formalization and implementation in Coq | ||
| + | ------- | ||
| + | 15h10-15h30 '''Coffee break''' | ||
| + | ------- | ||
| + | 15h30-17h10 <big><big>session 3</big></big><br> | ||
| + | 15h30-16h '''Sana Stojanovic, vesna Pavlovic and Predrag Janicic''': Automated generation of formal and readable proofs in geometry using coherent logic<br> | ||
| + | 16h05-16h35 '''Tuan Minh Pham''': An additional tool about the orientation for theorem proving in the Coq proof assistant <br> | ||
| + | 16h40-17h10 '''Laurent Fuchs and laurent Théry''': A formalization of Grassmann-Cayley Algebra in Coq | ||
| + | ----- | ||
| + | 17h20-18h '''Business Meeting''' | ||
<center><big><big><big>Friday, July 23</big></big></big></center> | <center><big><big><big>Friday, July 23</big></big></big></center> | ||
| − | + | --------------- | |
| + | 9h-10h40 <big><big>Session 4</big></big><br> | ||
| + | 9h-9h30 '''Dominique Michelucci''': What is a line ? <br> | ||
| + | 9h35-10h05 Daniel Lichtblau Midpoint locus of a triangle in a comer<br> | ||
| + | 10h10-10h40 '''Nico Magaud, Agathe Chollet and Laurent Fuchs''': Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective | ||
| + | --------------- | ||
| + | 10h40-11h '''Coffe break''' | ||
| + | |||
afternoon : tourism :-) | afternoon : tourism :-) | ||
Version du 17 mai 2010 à 08:37
9h-9h45 Registration
9h45-10h Welcome
10h-11h Invited Talk
Robert Joan-Arynio:
11h-11h20 Coffee break
11h20-12h30 session 1
11h20-11h50 Xiaoyu Chen: Formal representation and Automated transformation of geometric statements
11h55-12h25 Pedro Quaresma: TGTP - Thousands of geometric problems for geometric theorems provers
12h30-14h Lunch
14h-15h10 session 2
14h-14h30 Phil Scott and Jacques Fleuriot:Idle time discovery in geometry theorem proving
14h35-15h05 Jean Duprat: The Euclid's plane: formalization and implementation in Coq
15h10-15h30 Coffee break
15h30-17h10 session 3
15h30-16h Sana Stojanovic, vesna Pavlovic and Predrag Janicic: Automated generation of formal and readable proofs in geometry using coherent logic
16h05-16h35 Tuan Minh Pham: An additional tool about the orientation for theorem proving in the Coq proof assistant
16h40-17h10 Laurent Fuchs and laurent Théry: A formalization of Grassmann-Cayley Algebra in Coq
17h20-18h Business Meeting
9h-10h40 Session 4
9h-9h30 Dominique Michelucci: What is a line ?
9h35-10h05 Daniel Lichtblau Midpoint locus of a triangle in a comer
10h10-10h40 Nico Magaud, Agathe Chollet and Laurent Fuchs: Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
10h40-11h Coffe break
afternoon : tourism :-)
to be completed
