0
$\begingroup$


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

$\endgroup$
  • $\begingroup$ It might help to know what your final motivation is: are you asking whether you can represent and prove any property of FOPL in EL? The answer to that is yes (at least in theory). However the example you give is particularly simple: both hypotheses are Horn Clauses, which makes them rather natural to represent as reduction rules. $\endgroup$ – cody Apr 14 '14 at 14:38
  • $\begingroup$ My motivation is to use EL+ET to represent ontologies. Proofs can then be used to prove consistency of a particular ontology. Finally implementations can be developed that satisfy the axioms of an ontology. I have transformed many FOPL axioms to ET+EL, but I do not have any theoretical basis for such transformations. I am unsure if this approach is theoretically sound. Also, I am not sure of when to use either of the approaches mentioned in Q1 and Q2. I will post a more challenging example soon. $\endgroup$ – Pat Apr 14 '14 at 21:44
  • $\begingroup$ Your parentheses in the expression ((R x y) implies (R y z)) implies (R x z) worry me: implication associates to the right. Also worrisome is eq [e1] : R x X = true . This seems to imply that X is related to everyone, which is not the case in the exercise. $\endgroup$ – cody Apr 15 '14 at 21:24
  • $\begingroup$ You might want to look at the resolution rule, which is a very simple formulation of first order logic, and is probably a good candidate for performing "logic by rewriting". OTOH, there are some very nice resolution provers out there that perform quite well, so it might not even be useful to use CafeOBJ in this specific instance... $\endgroup$ – cody Apr 15 '14 at 21:29
  • $\begingroup$ You are correct, but I think these changes might be needed when moving from COQ to CafeOBJ. The additional brackets is my attempt to produce uncurried version of COQs implies connective. I do not think that symmetry and transitivity are enough to prove reflexivity. I think that I need some concrete X. $\endgroup$ – Pat Apr 15 '14 at 22:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.