Monday 25th September
09:00-10:00 | Invited Talk: Spatial Constraints on Lines by Christoph M. Hoffmann (Purdue University, USA) |
10:00-10:30 | Coffee Break |
10:30-11:00 | A New Heuristic to Identify Rigid Clusters by C. Jermann, G. Trombettoni, B. Neveu, and M. Rueher (France) |
11:00-11:30 | Hybrid Methods for Solving Geometric Constraint Systems by X.-S. Gao, L.-D. Huang, and K. Jiang (China) |
11:30-12:00 | Higher-order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry by C. Dehlinger, J.-F. Dufourd, and P. Schreck (France) |
12:00-12:30 | Emphasizing Human Techniques in Geometry Automated Theorem Proving: A Practical Realization by R. Caferra, N. Peltier, and F. Puitg (France) |
12:30-14:00 | Lunch |
14:00-14:20 | Morph Gentzen, KR, and Spatial World Models by C. F. Nourani (USA) |
14:20-14:40 | Constraint Satisfaction and Reasoning in Declarative Geometry with Intervals by E. Roukoleev and D. Ushakov (Russia) |
14:40-15:00 | Implementation of the Fast Schur-Cohn Algorithm on Schönhage's Multitape Turing Machine TP by C. Brunie (France) |
15:00-15:20 | Some Constructions for Birkhoff Bivariate Polynomial Interpolation by A. Campillo and S. Encinas (Spain) |
15:20-16:00 | Coffee Break |
16:00-16:30 | Solving the Birkhoff Interpolation Problem via the Critical Point Method: An Experimental Study by F. Rouillier, M. Safey El Din, and E. Schost (France) |
16:30-17:00 | A Practical Program of Automated Proving for a Class of Geometric Inequalities by L. Yang and J. Zhang (China) |
17:00- | Software Demo |
18:00- | Informal Workshop Dinner-Reception |
Tuesday 26th September
09:00-09:30 | Proving Real Geometry Theorems and the Computation of the Real Radical by P. Conti and C. Traverso (Italy) |
09:30-10:00 | Randomized Zero Testing of Radical Expressions and Elementary Geometry Theorem Proving by D. Tulone, C. Yap, and C. Li (USA) |
10:00-10:30 | The Kinds of Truth of Geometry Theorems by M. Bulmer, D. Fearnley-Sander, and T. Stokes (Australia) |
10:30-11:00 | Coffee Break |
11:00-11:30 | A Complex Change of Variables for Geometrical Reasoning by T. Stokes and M. Bulmer (Australia) |
11:30-12:00 | Remarks on Geometric Theorem Proving by L. Bazzotti, G. Dalzotto, and L. Robbiano (Italy) |
12:00-12:30 | Automated Reasoning about Surfaces (Progress Report) by D. Wang (France) |
12:30-14:00 | Lunch |
14:00-15:20 | Open Session Talk: Automated Deduction in Geometry and its Technological Applications by Wen-tsün Wu (Academia Sinica, China) |
15:20-15:40 | Open Session Demo: Geometry Expert by X.-S. Gao (China) |
15:40-16:00 | Open Session Demo: Cinderella by J. Richter-Gebert (Switzerland) |
16:00-16:45 | Apéro (Reception) |
17:00- | Guided Zurich Sightseeing with Dinner |
Wednesday 27th September
09:00-10:00 | Invited Talk: Effective Methods in Computational Synthetic Geometry by Jürgen Bokowski (Darmstadt University of Technology, Germany) |
10:00-10:30 | Coffee Break |
10:30-11:00 | Incidence Theorems on Manifolds by J. Richter-Gebert (Switzerland) |
11:00-11:30 | Decision Complexity in Dynamic Geometry by U. Kortenkamp and J. Richter-Gebert (Germany and Switzerland) |
11:30-12:00 | About Cedric by T. von Oertzen (Germany) |
12:00-12:30 | Automated Production of Readable Proofs for Theorems in Projective Geometry by H. Li and Y. Wu (China) |
12:30-14:00 | Lunch |
14:00-14:20 | On Minkovski Decompositions of Polytopes by G. Panina (Russia) |
14:20-14:40 | On Some Examples of Bilevel Programming Solved by a New Global Optimization Method by T.-J. Wu (China) |
14:40-15:00 | Reduced Form of Yang-Mills Equation of SU(3) on R^{4,0} by H. Shi and Y. Wu (China) |
15:00-15:30 | Coffee Break |
15:30-16:00 | Qubit Logic, Algebra and Geometry by T. Havel (USA) |
16:00-16:30 | Theorem Proving in Infinitesimal Geometry by J. D. Fleuriot (UK) |