Une structure de données pour représenter de grands ensembles de termes égaux : application à une méthode générale de simplification d'expressions

We introduce a new data structure, called collection of structures, to handle large --often infinite-- sets of terms, in order to efficiently simplify terms or expressions. We precisely define the semantics of collections of structures and we provide an optimal implementation thereof. We provide a careful complexity analysis of the new data structure as well as a detailed experimental evaluation of its efficiency. We use collections of structures to compute the congruence defined by a set of equations between terms with free variables, and a set of generators, in the case where the number of equivalence classes of the congruence is finite. This allows us to minimize expressions belonging to such a theory in linear time. For instance, the method applies to boolean expressions using no more than three distinct propositional variables. We modify the previous algorithm to make it able to simplify expressions in the context of more difficult situations where the number of equivalence classes is huge or infinite. We experimentally show that the modified algorithm is able to handle expressions using up to 100,000 symbols with up to 20 different propositional variables. The algorithm to compute the congruence generalizes the several existing methods to compute the congruence closure of a relation between ground terms, proposed in the literature, to non ground equations. We show that --when limited to ground equations-- our method is simpler to understand and, at the same time, as efficient than any previously proposed one. This thesis also contains an independent --and preliminary-- chapter devoted to the problem of computing the list of all prime implicants of a boolean formula in disjunctive normal form. We provide a survey of a significant number of methods proposed in the literature, in a unified way, using a single notation. We carefully prove the correctness of all methods and we experimentally compare their efficiency on the basis of a common compact internal representation of boolean formulas.Nous introduisons une nouvelle structure de données, appelée collection de structures, conçue dans le but de simplifier efficacement des expressions. Nous décrivons précisément sa sémantique et nous en donnons une implémentation optimale. Nous fournissons une étude détaillée de sa complexité théorique que nous complétons par une étude expérimentale approfondie. Nous utilisons les collections de structures pour calculer la congruence définie par un ensemble d’équations non closes et un ensemble de générateurs, lorsque cette congruence possède un nombre fini de classes d'équivalence. Ce résultat nous permet de minimiser en temps linéaire les expressions appartenant à de telles théories, par exemple, les expressions booléennes utilisant au plus trois variables propositionnelles distinctes. Nous étendons cet algorithme pour l'appliquer à des théories plus générales comportant trop de classes d'équivalence pour être représentables, en théorie ou en pratique. Nous obtenons ainsi un algorithme générique de simplification d'expressions dont nous démontrons l'utilité pratique en l'appliquant à la simplification d'expressions booléennes comportant jusqu'à 100.000 symboles et 20 variables propositionnelles. Notre algorithme de calcul de congruence généralise les algorithmes connus de fermeture congruente utilisés en démonstration automatique de théorème. Nous montrons que notre algorithme, basé sur les collections de structures, est plus simple à comprendre et tout aussi efficace que ces méthodes, pour la résolution d'équations closes entre termes. Indépendamment de ces développements, nous proposons, dans un chapitre préalable, une synthèse d'un ensemble significatif de méthodes de calcul de la liste des impliquants premiers des formules écrites sous forme normale disjonctive. Nous décrivons ces méthodes dans un cadre unifié et nous démontrons rigoureusement leur correction. Nous les implémentons en utilisant une représentation interne unique et nous comparons expérimentalement leur efficacité selon cette implémentation.(FSA - Sciences de l'ingénieur) -- UCL, 201