Automated Theorem Proving in Dynamic Geometry: Current Achievements

Special Session at ACA'2016
to be held August 1-4, 2016 in Kassel, Germany

Since the last half century, automated deduction in elementary geometry has become one of the most successful achievements in the field of automated reasoning. Along these decades various methods and techniques have been studied and developed for automated proving and discovering of elementary geometry statements. On the other hand, dynamic geometry software systems (DGS) have emerged, such as Cabri Geometry, C.a.R., Cinderella, DrGeo, GeoGebra, the Geometer's Sketchpad, Geometry Expert, Geometry Expressions or Kig with an ever-increasing presence in mathematics education. Some of them possess a large number of users (over thirty million) all around the world. The merging of these two tools (automatic proving and dynamic geometry) is, thus, a very natural, challenging and promising issue, currently involving logic, symbolic computation, software development, algebraic geometry and mathematics education experts all from over the world. In fact, a COST proposal for a EU network, involving all these agents, is in its way to be presented this year.

The Special Session intends to be a forum for 
  • presenting the current state of the art concerning the implementation of automatic proving features on dynamic geometry systems,
  • fostering a debate concerning the role and use of such features in mathematics education (in analogy with the debate, in the 80’s, about the use of calculators in the school),
  • acting as a kind of Early Kick Off meeting for the proposed COST network "I-geometrybook”.
Confirmed talks:

 Noah Dana-Picard (Jerusalem College of Technology, Israel),
Nurit Zehavi (Weizmann Institute of Science, Tel-Aviv, Israel):

Managing the constraints of technology for an automated study of envelopes (abstract)
 James Davenport (University of Bath, United Kingdom):
What does ‘without loss of generality’ mean? (abstract)
 Bernard Parisse (University of Grenoble, France):
About Giac's Gröbner basis and ideal elimination computation (abstract)
  Pedro Quaresma (University of Coimbra, Portugal):
Intelligent + Dynamic Geometry (abstract)
Eugenio Roanes-Lozano (Complutense University, Madrid, Spain):
A constructive approach to the cuadrics of revolution and their equations using the DGS GeoGebra (abstract)
 Thomas Sturm (LORIA, Nancy, France):
Towards higher-degree quantifier elimination by virtual substitution (abstract)
 Alfred Wassermann (University of Bayreuth, Germany):
sketchometry: a sketching tool for geometry (abstract)

If you are interested in proposing a talk, please send an abstract to the organizers. Please use the attached LaTeX template for your abstract and send the organizers both the LaTeX source and a compiled PDF version.

*First and third organizers partially supported by Spanish project MTM2014-54141-P (