[Maude-help] Using maude as a Formal calculus engine for Presburger Logic.

[LAPITRE Arnault]

Dear Maude help mailing list,

We on work on Verification, Validation and AAutomatic Testing of Formals 
Specification.
We develop some tools to do it in C++ using a Term Rewriting Engine 
(TRE) for terms simplification (like x+2x -> 3x) and Presburger tools 
(the Omega library: http://www.cs.umd.edu/projects/omega/) for formula 
analysis.

In 1998, When we had to choose a TRE for terms simplification, we have 
the choice between:

*** ELAN (the compiler doesn't support AC operators in 1998)

*** MAUDE (in 1998, Maude 1.0 has too much restiction for users like us, 
it wasn't free)

*** BRUTE (the TRE of CafeOBJ)
OUR CHOICE because it was efficiency and free in 1998.


Today we plane to replace BRUTE by another TRE because:
writing Term Rewriting Systems (TRS) for BRUTE is for us as programming 
in Assembly Language.

We want to use a new paradigm for our TRS conception with a tools more 
efficiency than BRUTE (it is so good).

We want to write:
1)++ TRS for terms simplification in Presburger Logic

2)++ TRS for Variables substitution by Terms in Terms T[v_1/t_1,...v_n/t_n]

3)++ TRS for alpha equivalence detection betwen terms

++ and much more

In June 2003, SURPRISE!!!!! Maude 2.0 is open source (GNU GPL2 Licence).

We plane to replace the TRE BRUTE by MAUDE, but we want to know if 
somebody has TRS to do (1), (2) or (3).
To Resume we need a TRS in MAUDE to perform good simplification in 
Presburger Formulae.

Do you have some links four us?

Do you have some recommandations to use MAUDE  as a server for 
terms simplification (communicated by unix pipe with our tools)?

Maude 2.0!!!!! A very good job.

-- 
Arnault LAPITRE

* Ingénieur - Chercheur
* CEA SACLAY
      Laboratoire Logiciels pour la Sûreté des Procédés
      Service Logiciels et Architectures
      CEA/DRT/LIST/DTSI/SLA/LLSP
      F-91191 GIF-SUR-YVETTE CEDEX
* Tél.: 01 69 08 34 22
* Fax : 01 69 08 20 82
* E-mail : arnault.lapitre at cea.fr