September 12
9:00-9:20 Opening (Dongming Wang)
Session 1 (Chair: Hongbo Li)
9:20-10:20 Plenary Talk Wen-tsün Wu and Mathematics Mechanization Xiao-Shan Gao
10:20-10:50 Break
10:50-11:50 Plenary Talk Around Dandelin-Gallucci Theorem Pascal Schreck
12:00 Lunch
Session 2 (Chair: Xiaoyu Chen)
2:00-2:30 Geometric search in TGTP Yannis Haralambous, Pedro Quaresma
2:30-3:00 Automated Geometer, a web-based discovery tool Francisco Botana, Zoltán Kovács, and Tomás Recio
3:00-3:30 User interface and operations of GeometryTouch on small and large touchscreens Wei Su, Chuan Cai and Jinzhao Wu
3:30-4:00 Break
Session 3 (Chair: Pascal Schreck)
4:00-4:30 Exploring algebraic tools for three-dimensional projective geometry Hongbo Li
4:30-5:00 br> N-dimension area method using exterior products V. Pavan
5:00-5:30 Computation of gcd chain over the power of an irreducible polynomial Xavier Dahan
5:40 Dinner
September 13
Session 4 (Chair: Dingkang Wang)
9:00-10:00 Plenary Talk Can You Pave the Plane Nicely with Identical Tiles Chuanming Zong
10:00-10:30 Break
10:30-11:30 Plenary Talk Interactive Theorem Proving in Geometry: From Foundations to Applications Jacques Fleuriot
11:40 Lunch
Session 5 (Chair: Jacques Fleuriot)
2:00-2:30 Mining geometry theorems in a regular polygon Zoltán Kovács
2:30-3:00 On n-sectors of the angles of an arbitrary triangle Dongming Wang, Bo Huang and Xiaoyu Chen
3:00-3:30 A system for automated deduction in engineering mechanics Philip Todd
3:30-4:00 Break
Session 6 (Chair: Jing Yang)
4:00-4:30 Towards a mechanisation in Isabelle of Birkhoff's ruler and protractor geometry Imogen I. Morris, Jacques D. Fleuriot
4:30-5:00 Mechanising an independent axiom system for Minkowski space-time Jake Palmer, Jacques D. Fleuriot
5:00-5:30 Verification of natural styled proofs in basic calculus using Maple Shuai Shi
5:30-6:30 ADG Business Meeting (Chair: Dongming Wang)
7:00 Conference Dinner
September 14
Session 7 (Chair: Dongming Wang)
9:00-10:00 Plenary Talk Comprehensive Gröbner Systems and Discovering Geometric Theorems Mechanically Dingkang Wang
10:00-10:30 Break
10:30-11:30 Plenary Talk Hard Combinatorial Problems via SAT Ilias Kotsireas
11:30-12:00 Closing (Dongming Wang)
12:00 Lunch