Oriented equational clauses as a programming language

Citations of this article
Mendeley users who have this article in their library.


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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free