On The Integration of Equality, Sorts, and Logic Programming

Logic programming in its original form lacks at least two important features that are predominant in the area of algebraic specifications of abstract data types: equations and a type concept. In this paper we consider many-sorted logic programs with equality. Besides the model-theoretic semantics based on initial models we investigate the operational semantics based on resolution and unification modulo a set of conditional equations. We define a translation of logic programs LP_E with equality into logic programs LP_ф with empty equational part and thus offer a rapid and correct realization of equational Horn logic. Correctness is achieved in the sense that the original program LP_E satisfies a goal G iff LP_ф. satisfies G.