A Hybrid Method for Finite Model Search in Equational Theories
Belaïd Benhamou, Laurent Hénocque · Fundamenta Informaticae · 1999
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 satisf