Unification, finite duality and projectivity in varieties of Heyting algebras (Q598304)

Addressed mainly to logicians, this article may also be of interest for computer scientists. Unification with respect to an equational theory was algebrized by the author [J. Log. Comput. 7, No. 6, 733--752 (1997; Zbl 0894.08004)] so as to utilize categorical duality theory for the determination of unification types in locally finite varieties of Heyting algebras, which is illustrated in the present paper. Although the unification algorithms that can indeed be extracted from this setting might be inefficient, the constructively found unification types may give a hint at a chance to improve the algorithms.