An application of automatic theorem proving in computer vision

Getting accurate construction of tridimensional CAD models is a field of great importance: with the increasing complexity of the models that modeling tools can manage nowadays, it becomes more and more necessary to construct geometrically accurate descriptions. Maybe the most promising technique, because of its full generality, is the use of automatic geometric tools: these can be used for checking the geometrical coherency and discovering geometrical properties of the model. In this paper, we describe an automatic method for constructing the model of a given geometrical configuration and for discovering the theorems of this configuration. This approach motivated by 3D modeling problems is based on characteristic set techniques and generic polynomials in the bracket algebra.