Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: interfacing Ocaml with Mathematica
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Elnatan Reisner <elnatan@c...>
Subject: Re: interfacing Ocaml with Mathematica
On Sep 7, 2010, at 6:00 AM, wrote:

> Date: Tue, 7 Sep 2010 06:36:35 +0200
> From: Basile Starynkevitch <>
> Subject: Re: [Caml-list] interfacing Ocaml with Mathematica
> To: zaid al-zobaidi <>
> Cc:
> Message-ID: <>
> Content-Type: text/plain; charset=US-ASCII
> On Fri, 03 Sep 2010 16:49:38 +0100
> zaid al-zobaidi <> 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.

Another possible route, although it might be overkill for your  
specific goal, would be to use an SMT solver.

Two popular ones are Z3 [1] and Yices [2], and both have OCaml APIs.  
CVC3 [3] is another one, this one open-source, with an old OCaml API  
[4], but I have no idea if it works---you'd have to try it or ask the  
author. (Maybe there's a newer OCaml API that I'm unaware of; I just  
found this with a quick Google.)