A hybrid method for finite model search in equational

• Autorzy: Benhamou B. , Henocque L.
• Języki publikacji: EN

Abstrakty

EN

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 ß 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

Słowa kluczowe

EN

finite model; equational theories; symmetry

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1999
• Tom: Vol. 39, Nr 1,2
• Strony: 21--38
• Opis fizyczny: bibliogr. 12 poz.

Twórcy

autor

Benhamou B.

autor

Henocque L.

• Laboratoire d'Informatique de Marseille, Centre de Mathématiques et d'Informatique, 39, rue Joliot Curie- 13453 Marseille cedex 13, France,