Sophie Tourret - Abduction en logique du premier ordre avec égalité

Cette thèse présente le résultat de mon travail sur la génération d'impliqués premiers en logique équationnelle fermée, i.e., la génération des conséquences les plus générales de formules logiques contenants des équations et des disequations entre termes sans variables. Ces travaux peuvent être divisé en trois parties. Tout d'abord, deux calculs de génération d'impliqués sont définis. Leur complétude pour la déduction est prouvée, ce qui signifie qu'ils sont tous deux capables de générer l'ensemble des impliqués modulo redondance d'une formule équationnelle fermée. Dans une deuxième partie, une structure de données arborescente est proposée pour stocker les impliqués générés, accompagnée d'algorithmes pour déceler les redondances et couper les branches de l'arbre lorsque c'est nécessaire. Cette structure de données est adaptée aux différents types de clauses (avec et sans symboles de fonctions, avec et sans contraintes) ainsi qu'aux différentes notions de redondance utilisées dans les calculs. En effet, chaque calcul utilise un critère de redondance légèrement différent des autres. Les preuves de correction et de terminaison des algorithmes sont fournies pour chaque algorithme. Enfin, une évaluation expérimentale des différentes méthodes de génération d'impliqués premiers est réalisée. Pour cela, un prototype de ces méthodes, écrit en Ocaml est comparé à des outils de génération d'impliqués premiers récents. Les résultats de ces expériences sont utilisés pour identifier les variantes les plus efficaces des algorithmes proposés. Les résultats son