In the Prolog language, Horn clauses of first-order logic are regarded as programs, and the resolution procedure is used as an interpreter. In this paper, we present the formalism of Horn oriented equational clauses (Horn clauses with a rewrite rule as the head part, and a list of equations as the body part). We show that such a formalism can be interpreted as a logic language with built-in equality, and that a procedure based on clausal superposition can be used as an interpreter. We define the operational, model-theoretic and fixpoint semantics of the language, and prove their equivalence. Then we point out the advantages of such a programming language: embodying Prolog, mixing functional and relational features and, handling the equality relation. Lastly, we present experiments performed with an implemented interpreter. © 1984.
Fribourg, L. (1984). Oriented equational clauses as a programming language. The Journal of Logic Programming, 1(2), 165–177. https://doi.org/10.1016/0743-1066(84)90003-7