A Hybrid Method for Finite Model Search in Equational Theories

Article type: Research Article

Authors: Benhamou, Belaid | Henocque, Laurent

Affiliations: Laboratoire d'Informatique de Marseille, Centre de Mathématiques et d'Informatique, 39, rue Joliot Curie - 13453 Marseille cedex 13, France. e-mail: Benhamou@gyptis.univ-mrs.fr e-mail: Henocque@esil.univ-mrs.fr

Note: [] Address for correspondence: Laboratoire d'Informatique de Marseille, Centre de Mathématiques et d'Informatique, 39, rue Joliot Curie - 13453 Marseille cedex 13, France

Abstract: Finite model and counter model generation is a potential alternative in automated theorem proving. In this paper, we introduce a system called FMSET which generates finite structures representing models of equational theories. FMSET performs a satisfiability test over a set of special first order clauses called “simple clauses”. The algorithm's originality stems from the combination of a standard enumeration technique and the use of first order resolution. Our objective is to obtain more propagations and still achieve good space and time complexity. Several experiments over a variety of problems have been pursued. FMSET uses symmetry to prune from the search tree unwanted isomorphic branches.

Keywords: Finite model, equational theories, symmetry

DOI: 10.3233/FI-1999-391202

Journal: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 21-38, 1999