<p><br/>
I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as  <a href="http://www.ldl.jaist.ac.jp/cafeobj/" rel="nofollow">CafeOBJ</a> . 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).
<a href="http://cseweb.ucsd.edu/~goguen/pubs/asbk.html" rel="nofollow">Goguen and Malcolm1</a> and <a href="http://cseweb.ucsd.edu/~goguen/sys/objcourse.html" rel="nofollow">Goguen and Malcolm2</a> describe FOPL as the <em>background</em> 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.
<br/>
I am using an example from <a href="http://coq.inria.fr/1-basic-Predicate-calculus" rel="nofollow">COQ: 1.4  predicate Calculus</a> 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.</p>

<p>Here is the description of the relation R from <a href="http://coq.inria.fr/1-basic-Predicate-calculus" rel="nofollow">COQ</a>.<br/></p>

<p>Hypothesis R_symmetric : $\forall x y:D, R x y \implies R y x$.<br/>
Hypothesis R_transitive : $\forall x y z:D, R x y \implies R y z \implies R x z$.<br/>
Prove that R is reflexive in any point x which has an R successor.<br/>
For any x and y, R x y implies R y x by symmetry, then by transitivity, we have R x x.<br/>
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).</p>

<p>Consider the 2 equations labelled PROPERTY in the module TRANSITIVE1 and EQUATION in the module TRANSITIVE2.</p>

<p>My questions are these: <br/>
<strong>Q1.</strong><br/>
Does the PROPERTY equation and its reduction represent and prove reflexivity? The results of the reductions would appear to represent a proof.
<br/>
<strong>Q2.</strong><br/>
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.<br/>
<strong>Q3.</strong><br/>
How do these approaches differ? Form my web searches I get <em>implicit</em> and <em>explicit</em> 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?</p>

<p>Regards,
Pat
<br/>
<code>
**> 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</p>

<p>**>  Replace COQ implies triplet with CafeOBJ conditional equation, using the following:
**>  [A -> B -> C] = [(A &amp; B) -> C] = [C = TRUE if (A &amp; 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
</code></p>

CC BY-SA 3.0
2014-04-14T14:38:54.453Z
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.
cody
CC BY-SA 3.0
2014-04-14T21:44:30.557Z
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.
Pat
CC BY-SA 3.0
2014-04-15T21:24:28.170Z
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.
cody
CC BY-SA 3.0
2014-04-15T21:29:05.447Z
You might want to look at the [resolution rule](http://en.wikipedia.org/wiki/Resolution_%28logic%29#Resolution_in_first_order_logic), 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*...
cody
CC BY-SA 3.0
2014-04-15T22:49:54.280Z
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.
Pat
CC BY-SA 3.0
2014-04-15T22:59:20.313Z
I take your point on theorem provers, and I generally use CafeOBJ's built-in OTTER-like prover to check my raw equational efforts. But I want to see how far one can get with just rewriting, ET+EL, and the proof score method of CafeOBJ/Goguen & Malcolm.
Pat
CC BY-SA 3.0
2014-04-16T06:17:49.963Z
[G&Ms](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.7321) approach to first order sentences in the context of algebraic semantics can be summarized:
1)Translate first order sentences into sequences of declarations and reduction.
2)Predicates are represented as Bool valued operations.
3)Assumptions are represented by constants or equations.
4)Goals are reductions in the context of a theory plus the assumptions.
5)Universal quantifiers in goals are handled by introducing new constants.
6)Existential quantifiers in assumptions are handled by introducing so called Skolem functions.
Pat
CC BY-SA 3.0
2014-04-16T17:15:42.777Z
For your example: you want to prove "if x is an arbitrary object related to *some other concrete object Y* (note the existential), then X is related to itself. I can also assure you that transitivity is $R(x,y) \Rightarrow (R(y, z)\Rightarrow R(x,z))$
cody
CC BY-SA 3.0
2014-04-16T17:16:35.863Z
let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/13937/discussion-between-cody-and-pat)
cody
<lo.logic><proofs>
Equational Logic and First Order Predicate Logic
Pat
# Equational Logic and First Order Predicate Logic

(Asked by: username_0 on 2014-04-14)

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as [CafeOBJ](http://www.ldl.jaist.ac.jp/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](http://cseweb.ucsd.edu/~goguen/pubs/asbk.html) and [Goguen and Malcolm2](http://cseweb.ucsd.edu/~goguen/sys/objcourse.html) 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](http://coq.inria.fr/1-basic-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](http://coq.inria.fr/1-basic-Predicate-calculus).

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

**Tags:** lo.logic, proofs
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_1**: 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.  
> **username_1**: You might want to look at the [resolution rule](http://en.wikipedia.org/wiki/Resolution_%28logic%29#Resolution_in_first_order_logic), 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*...  
> **username_0**: 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.  
> **username_0**: I take your point on theorem provers, and I generally use CafeOBJ's built-in OTTER-like prover to check my raw equational efforts. But I want to see how far one can get with just rewriting, ET+EL, and the proof score method of CafeOBJ/Goguen & Malcolm.  
> **username_0**: [G&Ms](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.7321) approach to first order sentences in the context of algebraic semantics can be summarized: 1)Translate first order sentences into sequences of declarations and reduction. 2)Predicates are represented as Bool valued operations. 3)Assumptions are represented by constants or equations. 4)Goals are reductions in the context of a theory plus the assumptions. 5)Universal quantifiers in goals are handled by introducing new constants. 6)Existential quantifiers in assumptions are handled by introducing so called Skolem functions.  
> **username_1**: For your example: you want to prove "if x is an arbitrary object related to *some other concrete object Y* (note the existential), then X is related to itself. I can also assure you that transitivity is $R(x,y) \Rightarrow (R(y, z)\Rightarrow R(x,z))$  
> **username_1**: let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/13937/discussion-between-cody-and-pat)  

---

## 0 answers

