Exemples de demonstration automatique en geometrie reelle
Institution:
Rennes 1Disciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
La these est consacree a l'etude de certains problemes de demonstration automatique en geometrie elementaire qui concernent des proprietes de natures reelles (existence d'intersections reelles, inegalites) et qui ne peuvent donc pas etre traitees par des methodes comme la methode de wu ou la methode des bases standard. Plus precisement on demontre par le calcul algebrique les proprietes suivantes: tout triangle a quatre cercles tritangents reels; le cercle circonscrit ne coupe pas le cercle inscrit mais coupe chacun des cercles exinscrits; le rayon du cercle inscrit est toujours inferieur ou egal a la moitie du rayon du cercle circonscrit. On dit qu'un cercle verifie la propriete p lorsque son rayon est inferieur a la moitie du cercle circonscrit. La methode de calcul qu'on utilise est basee sur les techniques de calcul formel sur les inegalites developpees depuis plusieurs annees a rennes (suites de sturm-habicht, etude de courbes). Ces calculs sont beaucoup trop importants pour etre menes a la main et sont donc effectues grace au systeme de calcul formel reduce (ces calculs en reduce sont donnes en annexe). On etudie les triangles avec un des cotes fixes et on identifie donc l'ensemble de ces triangles au plan affine. Des proprietes interessantes des triangles sont mises en evidence par les calculs faits. C'est ainsi qu'on peut montrer le resultat suivant: suivant la forme du triangle il existe un, deux ou trois cercles tritangents dont le rayon est inferieur ou egal a la moitie du rayon du cercle circonscrit