Plane Euclidean reasoning

An automatic reasoning system for plane Euclidean geometry should handle the wide variety of geometric concepts: points, vectors, angles, triangles, rectangles, circles, lines, parallelism, perpendicularity, area, orientation, inside and outside, similitudes, isometries, sine, cosine,... . It should be able to construct and transform geometric objects, to compute geometric quantities and to prove geometric theorems. It should be able to call upon geometric knowledge transparently when it is needed. In this paper a type of ring generated by points and numbers is presented which may provide a formal basis for reasoning systems that meet these requirements. The claim is that this simple algebraic structure embodies all the concepts and properties that are investigated in the many different theories of the Euclidean plane.