Déduction automatique en géométrie par réduction de figures

L'axiomatisation de la geometrie par euclide, et les differents travaux qui ont suivi, fournissent un sujet interessant de theories axiomatiques appliquees a l'informatique. Les methodes logiques et heuristiques, pour la resolution automatique en geometrie, suivent un raisonnement proche de celui du geometre. Bien que de telles demarches permettent une interpretation geometrique du raisonnement, ces approches sont peu efficaces et le plus souvent non deterministes. Les methodes algebriques, au contraire, sont de puissantes approches de deduction automatique en geometrie, mais elles ne laissent aucune trace lisible de la resolution qui n'est plus de nature geometrique. Des methodes de deduction basees sur des principes de reecriture sont des techniques efficaces pour la resolution de contraintes. Aussi avons nous porte notre interet sur une approche utilisant des techniques de reecriture pour la resolution de problemes en geometrie. Nous avons propose une methode pour les geometries d'incidence, projective et affine dans le plan. Elle consiste a traduire un probleme de geometrie en une certaine representation qui est une figure, une figure etant un ensemble fini de points et de droites dans une certaine relation. Des mecanismes de reecriture reduisent ces figures jusqu'a leur forme normale, et chaque pas de reduction correspond a un pas de preuve en geometrie. La forme normale de la figure associee a une proposition geometrique donnee determine si cette proposition est un theoreme. Les bonnes proprietes, de terminaison et de confluence, de la relation de reduction definie sont a l'origine du determinisme avec lequel la recherche automatique d'une demonstration peut etre effectuee