automatic construction of finite algebras

This paper deals withmodel generation for equational theories, i.e., automatically generating (finite) models of a given set of (logical) equations. Our method of finite model generation and a tool for automatic construction of finite algebras is described. Some examples are given to show the applications of our program. We argue that, the combination of model generators and theorem provers enables us to get a better understanding of logical theories. A brief comparison between our tool and other similar tools is also presented.