We show that some common varieties of modal K4-algebras have finitary unification type, thus providing effective best solutions for equations in free algebras. Applications to admissible inference rules are immediate.

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.