Oriented equational clauses as a programming language

AbstractIn 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