Equation solving in geometrical theories

Abstract

Incidence geometries of dimension two and three, miquelian geometry and projective geometry are defined through conditional equational axioms. The mechanization of these geometries is done using their associated positive/negative conditional term rewriting systems. To any figure and to any property of the figure are associated two terms t 1 and t2 such that the figure possesses the property if and only if tl and t2 have a same normal form for the conditional term rewriting system corresponding to the considered geometry.