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
(2018)
Files
these_atindehou.pdf
Open Access - Adobe PDF
- 1.65 MB
Details
- Authors
- Supervisors
- Abstract
- (fr) 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.
- Affiliations
Citations
Atindehou, M. M. (2018). 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. https://hdl.handle.net/2078.5/126362