What is the state of the art concerning automated geometry theorem provers (AGTP)?

I can see that a few computer algebra softwares and dynamic geometry softwares (e.g. geogebra) have embedded provers but I failed to find a comparison of these solvers nor a thorough list of AGTP.

Are there still AGTP using the quantifier elimination method of Tarski and its refinement such as cylindrical algebraic decomposition, or has it been superseded by other methods such as Wu-Ritts or Grobner bases?


There is the work of Narboux and collaborators on those topics, see e.g. his software page http://dpt-info.u-strasbg.fr/~narboux/software.html and his papers too.

I don't know if there's a paper comparing everything, but perhaps his last one with Boutry and Braun fits the bill https://hal.inria.fr/hal-01483457

  • $\begingroup$ Narboux et al. have written a nice overview of the subject in Chapter 2 of the Handbook of Geometric Constraint Systems Principles. $\endgroup$ – Timothy Chow Nov 4 '19 at 16:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.