Reasoning by symmetry and function ordering in finite model generation

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.