Name
Abstract | ||
|---|---|---|
Finite modele search for first order logic theories is a complementary alternative to automated deduction. Systems like Falcon, SEM and FMSET use the LNH(Least Number Heuristic) heuristic to eliminate some trivial symmetries. Such symmetries are worthful, but their exploitation is limited to the first levels of the model search tree, since they desappear as soon as the first cells have been instanciated. We study in this paper a more general notion of symmetry than LNH and provide some exploitations which we combine with it to optimize the symmetry use and increase the model search efficiency. The method SEM with and without symmetry is experimented on several interesting mathematic problems to show the advantage of symmetry. |
Year | Venue | Keywords |
|---|---|---|
2001 | JFPLC | symmetries,mots-clés :modèles finis,symétries keywords: finite models,automated deduction,first order logic |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
7 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Audemard | 1 | 640 | 37.66 |
| Belaid Benhamou | 2 | 174 | 21.85 |