Equational Logic and First Order Predicate Logic

Question

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as CafeOBJ . I wish to use ET+EL to represent and prove sentences in First Order Predicate Logic (FOPL). The advantage of such an approach is that one can easily map loose theories written pseudo-FOPL to more concrete theories which may have initial models (using views). Translating FOPL to EL seems to require auxiliary techniques such as Skolemization and sentences splitting. I am concerned that there maybe some FOPL sentences which cannot be represented using EL even using these auxiliary techniques. I am aware that in general EL is regarded as a sub-logic of FOPL and any valid EL theorem is a valid FOPL theorem (but not vice versa). Goguen and Malcolm1 and Goguen and Malcolm2 describe FOPL as the background for equational proof scores in OBJ which was a predecessor of CafeOBJ/Maude. They also provide general advice on how use EL to prove FOPL theorems.
I am using an example from COQ: 1.4 predicate Calculus which I have written as two CafeOBJ theories or loose specifications. They are my two attempts to represent FOPL in EL. I am not sure if the approaches are valid.

Here is the description of the relation R from COQ.

Hypothesis R_symmetric : $\forall x y:D, R x y \implies R y x$.
Hypothesis R_transitive : $\forall x y z:D, R x y \implies R y z \implies R x z$.
Prove that R is reflexive in any point x which has an R successor.
For any x and y, R x y implies R y x by symmetry, then by transitivity, we have R x x.
Symmetry and transitivity are not enough to prove reflexivity, we must also assume the x is related to something (e.g R x ? or R ? x exists).

Consider the 2 equations labelled PROPERTY in the module TRANSITIVE1 and EQUATION in the module TRANSITIVE2.

My questions are these:
Q1.
Does the PROPERTY equation and its reduction represent and prove reflexivity? The results of the reductions would appear to represent a proof.
Q2.
Does the reduction of the EQUATION in TRANSITIVE2 prove reflexivity? I use a form selective application of bi-directional rewriting. This form of rewriting is highly controller by the user. Space does not permit a full description, but in this case the condition in the EQUATION is executed first and the assumption R x Y is applied during the rewriting process. We could describe this as a manual proof with some machine support.
Q3.
How do these approaches differ? Form my web searches I get implicit and explicit as follows: The implicitly specification of function or relation asserts property that its value must satisfy. Implicit definitions take the form of a logical predicate over the input and result variables gives the result's properties. This approach seems to be distinct from the normal Peano style equational axioms (e.g. N + 0 = N). The PROPERTY approach seems to fit this description. Explicitly defined functions or relations are those where the definition can be used to to calculate an output from the arguments. The EQUATION approach seems to fit this description. Are these reasonable distinctions?

Regards, Pat
**> This is a loose module describing all models where the equation labelled PROPERTY holds. mod* TRANSITIVE1 { **> One sort or type called D. [ D ] **> A constant which ensures that transitivity holds op Y : -> D **> The symmetric property is asserted by CafeOBJ's commutativity property. op R__ : D D -> Bool {comm} op P : D D D -> Bool vars x y z : D **> Right associativity of implies eq [PROPERTY] : P(x,z,y) = (R x y) implies (R y z) implies (R x z) . } **> Normal rewriting open TRANSITIVE1 . red P(x,Y,x) . -- Gives true close **> A loose module describing all models where the equation labelled EQUATION holds. mod* TRANSITIVE2 { [ D ] op R__ : D D -> Bool {comm} op P : D D D -> Bool vars x y z : D

**> Replace COQ implies triplet with CafeOBJ conditional equation, using the following: **> [A -> B -> C] = [(A & B) -> C] = [C = TRUE if (A & B)] ceq [EQUATION] : R x z = true if ((R x y) and (R y z)) . **> Normal rewriting cannot deal with extra variable y in the condition on the RHS. **> Hence user controlled rewriting required using start/apply commands. } open TRANSITIVE2 . **> Using start/apply op X : -> D . **> If any variable x is related to arbitrary constant X eq [e1] : R x X = true . **> Then x is related to itself. **> CafeOBJ's start/apply commands allow selective bi-directional rewriting start R x x . apply .EQUATION with y = X at term . apply reduce at term . -- Result true : Bool close