Name
Abstract | ||
|---|---|---|
Finite model search for first-order logic theories is comple- mentary to theorem proving. Systems like Falcon, SEM and FMSET use the known LNH (Least Number Heuristic) heuristic to eliminate some trivial symmetries. Such symmetries are worthy, but their exploitation is limited to the first levels of the model search tree, since they disappear as soon as the first cells have been interpreted. The symmetry property is well-studied in propositional logic and CSPs, but only few trivial results on this are known on model generation in first-order logic. We study in this paper both an ordering strategy that selects the next terms to be interpreted and a more general notion of symmetry for finite model search in first-order logic. We give an ecient detection method for such symmetry and show its combination with the trivial one used by LNH and LNHO heuristics. This increases the eciency of finite model search generation. The method SEM with and without both the function ordering and symmetry detection is experimented on several interesting mathematical problems to show the advantage of reasoning by symmetry and the function ordering. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-45620-1_19 | CADE |
Keywords | Field | DocType |
function ordering,finite model generation,first order logic,propositional logic,theorem proving | Discrete mathematics,Heuristic,Computer science,Automated theorem proving,Algorithm,Propositional calculus,First-order logic,Homogeneous space,Search tree | Conference |
ISBN | Citations | PageRank |
3-540-43931-5 | 5 | 0.45 |
References | Authors | |
11 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Audemard | 1 | 640 | 37.66 |
| Belaid Benhamou | 2 | 174 | 21.85 |