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: Dandelin-Gallucci's theorem. We work in the very simple but powerful framework of projective incidence geometry, where only incidence relationships are considered. We study and compare two new and very different approaches to prove this theorem. First, we propose a new proof based on the well-known Wu's method. Second, we use an original method based on matroid theory to generate a proof script which is then checked by the Coq proof assistant. For each method, we point out which parts of the proof we manage to carry out automatically and which parts are more difficult to automate and require human interaction. We hope these first developments will lead to formally proving more 3D theorems automatically and that it will be used to formally verify some key properties of computational geometry algorithms in 3D.

Constraint satisfaction problems related to geometry mostly arise in CAD. But even though they are designed for geometry, none of the methods proposed to solve these problems fully meets the requirements needed by the educational domain. In this paper, we adapt CAD methods to education and show that results must be construction programs in order to take into account particular cases. We present then a framework implemented in Prolog as a knowledge-based system called Progé.

International audience

This paper presents some important issues and potential research tracks for Geometric Constraint Solving: the use of the simplicial Bernstein base to reduce the wrapping effect in interval methods, the computation of the dimension of the solution set with methods used to measure the dimension of fractals, the pitfalls of graph based decomposition methods, the alternative provided by linear algebra, the witness configuration method, the use of randomized provers to detect dependences between constraints, the study of incidence constraints, the search for intrinsic (coordinate-free) formulations and the need for formal specifications.

Many authors have so far studied the problem of geometric construction in CAD from a combinatorial point of view. The derived algorithms are efficient but not general enough. Moreover the problem of robustness is seldom mentioned. We expose a logical framework of geometric construction which points out the difficulties to overcome in order to implement a correct geometric universe. We think that this precise study of the particularities of geometry is necessary to obtain a robust geometric solver.