Maude-help mailing list

[PATRICK BROWNE <patrick.browne AT dit.ie>]

***(
Dear list,
I am interested in the relationship between First Order Predicate Logic (FOPL) and Maude's Equational Logic (EL).
I am aware that in general EL is regarded as a sub-logic of FOPL. But I am concerned with the precise machine support for FOPL in OBJ-like languages.
Goguen and Malcolm [1] describe FOPL as the "background" for proof scores in OBJ.

I am using an example from COQ[2] which I have written as Maude theory or  loose specification
Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> 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).

My questions are these:
Does the PROPERTY equation and its reduction represent and prove reflexivity?
If it does what is the general description of such proofs, they seem to be distinct from the normal Peano style equations.
I know reflexivity cannot be proved by rewriting with EQUATION.
Can reflexivity be proved using EQUATION together with Maude's Inductive Theorem Prover (ITP) or perhaps with CafeOBJ's 'apply' command?
Regards,
Pat
 

[1] Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, page 85, http://cseweb.ucsd.edu/~goguen/sys/objcourse.html
[2] "1.4  predicate Calculus." http://coq.inria.fr/1-basic-predicate-calculus


)


fth TRANSITIVE is
pr(BOOL) .
sort D .
***> A constant which ensures that transitivity holds
op Y : -> D .
***> The symmetric property is asserted by Maude commutativity property.
op R__ : D D -> Bool [comm] .
op P : D D D -> Bool .
vars x y z : D
eq [PROPERTY] : P(x,z,y)  =  ((R x y) implies (R y z)) implies (R x z) .
***> Normal rewriting cannot deal with extra variable y in the condition of the transitivity axiom.
***> ceq [EQUATION] : R x z = true if (R x y) and (R y z) [nonexec label transitive] .
endfth

red P(x,x,Y) .
red P(x,x,Y) implies R x x .

This email originated from DIT. If you received this email in error, please delete it from your system. Please note that if you are not the named addressee, disclosing, copying, distributing or taking any action based on the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to Grangegorman