On Fri, 03 Sep 2010 16:49:38 +0100
zaid al-zobaidi <Z.K.Ibrahim@cs.bham.ac.uk> wrote:

> Dear members
> 
> I am writing an Ocaml code and part of it I need to do the following job:
> 
> * I want to find out if two arithmetic or logical expressions  are equal
>   like "a + b" and "2 * a + b - a" or "a and b or a" and "a", and Ocaml

So you want a formal tool working on formal expression trees [you don't want to work on strings]. I believe there are several of these.

And there exist a limitation on them. IIRC, one of Robinson's theorems states that under suitable & reasonable hypothesis the formal equality problem is undecidable (perhaps: equality of functions expressed with an expression made from an unknown x, constants, four usual operations + - * /, square roots, trigonometric, logarithmic, exponential, ... is undecidable)

On the other hand, rewriting such a simplification tool by yourself is a very interesting exercise.

> it is unlikely to achieve my target, therefore I checked the available
> packages and tools that can do the job and I found "Mathematica".
> I would appreciate if someone could guide me on how to interface (if
> possible)to mathematica from Ocaml programme.
> 

I would choose another tool than Mathematica. I would choose a free (as in speech) software. Very probably, Coq could be used that way (Coq is coded in & interfaced with Ocaml). 
But I don't know it well enough. Coq is a world by itself.

Cheers

-- 
Basile Starynkevitch <basile@starynkevitch.net>