We discuss various semantics of many-sorted logic programs with equality both from the viewpoint of algebraic specifications as well as from the viewpoint of logic programming. We define model-theoretic semantics based on initial models, least generalized Herbrand models and a least fixpoint construction, and we investigate proof-theoretic semantics based on resolution and unification modulo a set of conditional equations. Generalizing ordinary SLD derivations, we introduce so-called SLDE derivations and SLDE trees and study their correctness and completeness properties. We define a translation of logic programs LP_E with equality into equivalent logic programs LP_ø with empty equational part such that LP_E satisfies a goal G if and only if LP_ø satisfies G.