ADG 2010 - Munich
ADG 2010 - Munich
Différences entre les versions de « Schedule »
De ADG 2010 - Munich
| Ligne 8 : | Ligne 8 : | ||
11h-11h20 '''Coffee break''' | 11h-11h20 '''Coffee break''' | ||
---- | ---- | ||
| − | 11h20-12h30 <big><big> | + | 11h20-12h30<center> <big><big>'''Session 1'''</big></big></center><br> |
| − | 11h20-11h50 '''Xiaoyu Chen''': Formal representation and Automated transformation of geometric statements <br> | + | 11h20-11h50 <br> |
| − | 11h55-12h25 '''Pedro Quaresma''': TGTP - Thousands of geometric problems for geometric theorems provers | + | '''Xiaoyu Chen''': Formal representation and Automated transformation of geometric statements <br> |
| + | 11h55-12h25 <br> | ||
| + | '''Pedro Quaresma''': TGTP - Thousands of geometric problems for geometric theorems provers | ||
------------ | ------------ | ||
<br> | <br> | ||
| Ligne 16 : | Ligne 18 : | ||
<br> | <br> | ||
------------- | ------------- | ||
| − | 14h-15h10 <big><big> | + | 14h-15h10 <center><big><big>'''Session 2'''</big></big></center><br> |
14h-14h30 '''Phil Scott and Jacques Fleuriot:'''Idle time discovery in geometry theorem proving <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 | 14h35-15h05 '''Jean Duprat''': The Euclid's plane: formalization and implementation in Coq | ||
| Ligne 22 : | Ligne 24 : | ||
15h10-15h30 '''Coffee break''' | 15h10-15h30 '''Coffee break''' | ||
------- | ------- | ||
| − | 15h30-17h10 <big><big> | + | 15h30-17h10 <center><big><big>'''Session 3'''</big></big></center><br> |
15h30-16h '''Sana Stojanovic, vesna Pavlovic and Predrag Janicic''': Automated generation of formal and readable proofs in geometry using coherent logic<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> | 16h05-16h35 '''Tuan Minh Pham''': An additional tool about the orientation for theorem proving in the Coq proof assistant <br> | ||
| Ligne 31 : | Ligne 33 : | ||
<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-10h40 <center><big><big>'''Session 4'''</big></big></center><br> |
9h-9h30 '''Dominique Michelucci''': What is a line ? <br> | 9h-9h30 '''Dominique Michelucci''': What is a line ? <br> | ||
9h35-10h05 Daniel Lichtblau Midpoint locus of a triangle in a comer<br> | 9h35-10h05 Daniel Lichtblau Midpoint locus of a triangle in a comer<br> | ||
| Ligne 38 : | Ligne 40 : | ||
10h40-11h '''Coffe break''' | 10h40-11h '''Coffe break''' | ||
----- | ----- | ||
| − | 11h- | + | 11h-12h40 <center><big><big>'''Session 5'''</big></big></center><br> |
| + | 11h-11h30 '''Pavel Pech''': Equivalent formulas for a quadrilateral being cyclic <br> | ||
11h35-12h05 '''Simon Thierry, Pascal Schreck and Pascal Mathis''': Why under-constrained systems are not that bad<br> | 11h35-12h05 '''Simon Thierry, Pascal Schreck and Pascal Mathis''': Why under-constrained systems are not that bad<br> | ||
12h10-12h40 '''Fadoua Ghourabi, Tetsuo Ida and Asem Kasem''': Proof documents of Origami theorems. | 12h10-12h40 '''Fadoua Ghourabi, Tetsuo Ida and Asem Kasem''': Proof documents of Origami theorems. | ||
| Ligne 47 : | Ligne 50 : | ||
---- | ---- | ||
| − | + | 9h-10h40<center><big><big>'''Session 6'''</big></big></center><br> | |
| + | 9h-9h30 | ||
| + | '''Tomas Reccio, Rafael Losada and Jose Luis Valcarce''': On the automatic discovery of Steiner-Lehmus generalizations<br> | ||
| + | 9h35-10h05 '''Susanne Apel and Jürgen Richter-Gebert''': Cancellation patterns in automatic geometric theorem proving<br> | ||
| + | 10h10-10h40 '''Zou Yu and Zhang Jingzhong''': Readable Machine proofs for particle geometry<br> | ||
| + | ---- | ||
| + | 10h40-11h '''Coffee break''' | ||
| + | ---- | ||
| + | 11h - 12h40 | ||
| + | <center><big><big>'''Session 7'''</big></big></center> | ||
| + | 11h-11h30 | ||
| + | '''Francisco Botana, José Luis Valcarce, Miguel A. Abadanades and Jesus Escribano''': On perfprming automatic discovery in dynamic geometry environments<br> | ||
| + | 11h35-12h05 | ||
| + | '''Thorsten Orendt''': On the complexity of the reachability problem in dynamic geometry<br> | ||
| + | 12h10-12h40 | ||
| + | '''Michael Gerhaüser and Alfred Wassermann''': Autmatic calculation of plane loci using Groebner bases and integration into a dynamic geometryc system | ||
| + | ---- | ||
| + | 12h40 - : '''Lunch''' | ||
<center><big><big><big>Saturday, July 24</big></big></big></center> | <center><big><big><big>Saturday, July 24</big></big></big></center> | ||
| − | |||
| − | |||
Version du 17 mai 2010 à 09:10
9h-9h45 Registration
9h45-10h Welcome
10h-11h Invited Talk
Robert Joan-Arynio:
11h-11h20 Coffee break
11h20-12h30
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
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
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
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
11h-12h40
11h-11h30 Pavel Pech: Equivalent formulas for a quadrilateral being cyclic
11h35-12h05 Simon Thierry, Pascal Schreck and Pascal Mathis: Why under-constrained systems are not that bad
12h10-12h40 Fadoua Ghourabi, Tetsuo Ida and Asem Kasem: Proof documents of Origami theorems.
12h40- : Lunch
afternoon : tourism + social event
9h-10h40
9h-9h30
Tomas Reccio, Rafael Losada and Jose Luis Valcarce: On the automatic discovery of Steiner-Lehmus generalizations
9h35-10h05 Susanne Apel and Jürgen Richter-Gebert: Cancellation patterns in automatic geometric theorem proving
10h10-10h40 Zou Yu and Zhang Jingzhong: Readable Machine proofs for particle geometry
10h40-11h Coffee break
11h - 12h40
11h-11h30
Francisco Botana, José Luis Valcarce, Miguel A. Abadanades and Jesus Escribano: On perfprming automatic discovery in dynamic geometry environments
11h35-12h05
Thorsten Orendt: On the complexity of the reachability problem in dynamic geometry
12h10-12h40
Michael Gerhaüser and Alfred Wassermann: Autmatic calculation of plane loci using Groebner bases and integration into a dynamic geometryc system
12h40 - : Lunch
