简介:Thispaperdealswithmodelgenerationforequationaltheories,i.e.,automaticallygenerating(finite)modelsofagivensetof(logical)equations.Ourmethodoffinitemodelgenerationandatoolforautomaticconstructionoffinitealgebrasisdescribed.Someexamplesaregiventoshowtheapplicationsofourprogram.Wearguethat,thecombinationofmodelgeneratorsandtheoremproversenablesustogetabetterunderstandingoflogicaltheories.Abriefcomparisonbetwweenourtoolandothersimilartoolsisalsopresented.