Ghilardi, Silvio Unification through projectivity. (English) Zbl 0894.08004 J. Log. Comput. 7, No. 6, 733-752 (1997). 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) Cited in 3 ReviewsCited in 37 Documents 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) Keywords:E-unification; algebraic approach to unification under equational conditions; finitely presented algebra; projective algebra; categorical equivalence; Brouwerian semilattices PDFBibTeX XMLCite \textit{S. Ghilardi}, J. Log. Comput. 7, No. 6, 733--752 (1997; Zbl 0894.08004) Full Text: DOI