Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Reasoning by Symmetry and Function Ordering in Finite Model Generation
| |
|
Reasoning by Symmetry and Function Ordering in Finite Model Generation
Gilles Audemard2, 3  and Belaid Benhamou3
| (2) |
ITC-IRST, via Sommarive 16, 38050 Povo, Trento, Italy |
| (3) |
Laboratoire des Sciences de l’Information et des Systèmes de Marseille (LSIS), 39, Rue Joliot Curie, 13453 Marseille cedex 13, France |
Abstract
Finite model search for first-order logic theories is complementary 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 efficient detection method for such symmetry and show its
combination with the trivial one used by LNH and LNHO heuristics. This increases the efficiency 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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|