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)

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: DOI