  We show that the set of all formulas in n variables valid in a finite class A
of finite algebras is always a regular tree language, and compute a finite
axiom set for A. We give a rational reconstruction of Barzdins' liquid flow
algorithm (Barzdin+Barzdin, 1991). We show a sufficient condition for the
existence of a class A of prototype algebras for a given theory T. Such a set
allows us to prove T |= p simply by testing whether p holds in A.
