The Handbook of Geometric Constraint Systems Principles is an entry point to the currently
used principal mathematical and computational tools and techniques of the geometric …

This paper describes the formalization of the arithmetization of Euclidean plane geometry in
the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for …

In this paper, we report on the formal proof that Hilbert's axiom system can be derived from
Tarski's system. For this purpose we mechanized the proofs of the first twelve chapters of …

We compare the pencil/paper proofs and formal proof of two traditional proofs in high school
geometry. We highlight the fact that slightly different formulations or proofs can lead to …

We describe our ongoing project of formalization of algebraic methods for geometry theorem
proving (Wu's method and the Groebner bases method), their implementation and …

This paper describes some techniques to help building formal proofs in geometry and at the
same time improving readability. Rather than trying to completely automate the proving …

The pursuit of an Intelligent and Dynamic Geometry Book should involve the study of how
currently developing methodologies and technologies of geometry knowledge …

The geometry automated theorem proving area distinguishes itself by a large number of
specific methods and implementations, different approaches (synthetic, algebraic, semi …

Mechanizing proofs of geometric theorems in 3D is significantly more challenging than in
2D. As a first noteworthy case study, we consider an iconic theorem of 3D geometry …

Over the last sixty years, a number of methods for automated theorem proving in geometry,
especially Euclidean geometry, have been developed. Almost all of them focus on …