[Maude-help] Using maude as a Formal calculus engine for Presburger Logic.
lapitre at albatros.saclay.cea.fr
Wed Jul 9 09:33:18 CDT 2003
Dear Maude help mailing list,
We on work on Verification, Validation and AAutomatic Testing of Formals
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
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
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.
* Ingénieur - Chercheur
* CEA SACLAY
Laboratoire Logiciels pour la Sûreté des Procédés
Service Logiciels et Architectures
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
More information about the Maude-help