Diagrammatic Reasoning in Projective Geometry

The heart of our thesis is that matrices of incidence can be used for mechanical theorem proving in projective geometry. To every geometrical statement of projective geometry is associated a matrix of incidence whose normal form is computed after successive identifications of rows and columns. Our main result is that the geometrical statement implies such or such property (incidence between a point and a line) if and only if the normal form of the associated matrix contains a 1 at such or such entry. 1 Introduction Diagrammatic representation appears in many human activities: mathematics, physics, economics, politics, etc. It constitutes a natural framework for the formalization and the mechanization of reasoning. As an example, Euclid, pioneer of the formal methods at the beginnings of the study of the algorithms, took advantage, proving the theorems of his geometry, of the visual properties of the geometrical figures. It is generally believed that figures are informal objects and th..