Abstract FR:

Cette these decrit la conception, la realisation et les applications d'une base de donnees deductive pour les relations mathematiques. Les relations stockees sont des egalites, des inegalites ou toutes autres relations mathematiques. Chaque relation est associee a ses conditions de validite. On peut stocker aussi bien la primitive d'une fonction, que la valeur d'une integrale definie ou que des inegalites bien connues. Un exemple de donnee est l'inegalite log(x) > 0 associee a sa condition de validite x > 1. Une requete consiste en une relation (eventuellement associee a une condition de validite), la base recherche alors parmi les donnees stockees les relations dont la requete est une instance. La reponse de la base a une requete est le resultat de l'instanciation, les conditions de validite apparaissent dans le resultat, garantissant ainsi les relations obtenues. La deduction consiste a simplifier les conditions de validite a l'aide des relations stockees. Le mecanisme de recherche d'une relation parmi les donnees utilise un processus d'unification en deux temps. La premiere etape est un calcul d'unificateurs modulo associativite et commutativite (ac) qui conserve les couples menant a l'echec du processus d'ac-unification. Dans un second temps, on tente de reduire ces echecs en les traitant soit comme des equations lineaires, soit par paramodulation avec les egalites stockees. Dans tous les cas les conditions de validite associees aux unificateurs calcules sont conservees avec la substitution correspondante et finalement apparaissent dans la reponse fournie par la base. Les applications d'une telle base de donnees sont nombreuses et touchent des domaines varies comme les systemes de calcul formel, la collaboration de solveurs de contraintes, les ouvrages electroniques consacres aux mathematiques,. . .