Logic program semantics for programming with equations

Abstract

We consider logic programming-like systems which are based on solving equations in a given structure as opposed to obtaining unifiers. While such systems are elegant from an operational point of view, a logical interpretation of the programs is not always apparent. In this paper, we restrict ourselves to the class of structures ℜ satisfying the eliminable variable property: we can construct an explicit definition, in the form of one system of equations, of the set of solutions to any ℜ-solvable system of equations. Correspondingly, we consider only the class of equality theories E such that every E-unifiable system of equations has an E-mgu. We then state three properties which provide basic relationships between E and ℜ. We prove that their satisfaction establishes an equivalence between a program considered as an equation solving engine (with respect to a structure) and the program considered as a logic program (with respect to a corresponding equality theory). A logical basis for these programs is thus given.