zbMATH — the first resource for mathematics

Unification through projectivity. (English) Zbl 0894.08004
The author proposes a new algebraic approach to unification under equational conditions. A unification problem is represented as a finitely presented algebra $$A$$, and a unifier for $$A$$ is a morphism from $$A$$ to some finitely presented projective algebra. This concept can be used to determine the unification types of various classes of algebras via categorical equivalence, e.g., for the variety of distributive lattices; for the variety of Brouwerian semilattices, a unification type is established which is, in a sense, stable under adjunction of extra constants.
Reviewer: M.Armbrust (Köln)

MSC:
 08A70 Applications of universal algebra in computer science 03B35 Mechanization of proofs and logical operations 68W30 Symbolic computation and algebraic computation 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: