The program and the abstracts of all talks collected in a single file: Program.pdf.

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 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
Comprehesive 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