Etude des symétries dans les modèles finis / Study of symmetries in finite models
In: Programmation en logique avec contraintes (Paris, 24-27 avril 2001 ) :109-122
Konferenz
- print, 9 ref
Zugriff:
La génération de modèles et de contre modèles finis pour des théories de la logique du premier ordre est une notion complémentaire à la démonstration automatique. Les méthodes de génération de modèles finis exploitent certaines symétries pour élaguer l'espace de recherche. Les systèmes FALCON, SEM et FMSET, utilisent l'heuristique LNH(Least Number Heuristic) de Jian ZHANG qui consiste a conserver les symétries existant entre les individus des domaines de la formule de départ. Bien qu'intéressantes, ces symétries triviales disparaissent sitôt qu'on avance dans la recherche de la solution. Les individus utilisés dans l'interprétation partielle deviennent non symétriques au sens LNH. Or d'autres symétries existent abondamment sur ces éléments. Nous étudions, dans ce papier un cadre plus général de la symétrie pour les modèles finis, nous montrons que la symétrie LNH est un cas particulier de ce cadre. Nous Donnons quelques résultats sur les symétries et proposons une méthode de détection dynamique de ces dernières. Nous expliquons ensuite comment utiliser ces symétries en les combinant avec celle de LNH pour améliorer l'efficacité des générateurs de modèles finis. Enfin, Une étude expérimentale et comparative de la méthode SEM avec et sans l'apport des symétries est faite sur des problèmes intéressants en mathématiques.
Titel: |
Etude des symétries dans les modèles finis / Study of symmetries in finite models
|
---|---|
Autor/in / Beteiligte Person: | AUDEMARD, Gilles ; BENHAMOU, Belaid |
Link: | |
Quelle: | Programmation en logique avec contraintes (Paris, 24-27 avril 2001 ) :109-122 |
Veröffentlichung: | Paris: Hermès Sciences, 2001 |
Medientyp: | Konferenz |
Umfang: | print, 9 ref |
Schlagwort: |
|
Sonstiges: |
|