From: Richard Fateman <fateman@cs.berkeley.edu>
Subject: Re: Algebraic Expression Simplifier
Date: Thu, 14 Sep 2000 09:40:58 -0700
Newsgroups: sci.math.symbolic
Summary: [missing]

Silvius Rus's question is kind of vague, so it is hard to know for
sure, but I think the results on Presburger arithmetic are probably
NOT what is  wanted.  On the other hand, some of it may be relevant.



john green wrote:
> 
> Silvius Rus <rus@tamu.edu> writes:
> 
> > Can anyone please point me to a software package (within academia, if
> > possible) that can deal with symbolic integer expressions containing
> > arithmetic operators +, -, *, / and logical operators AND, OR, NOT.

"deal with"?  presumably you also have at least one variable. The
example
you give suggests at least 2 variables.  Are the variables also integer
valued,
or may they be thought of as indeterminates over the reals, complexes,
or
some other domain?

> >
> > What I need to do is store them (expressions) in a standard form so that
> > I can do quick comparisons.  That implies simplification, for instance
> > it should realize that { a < b AND a<>b }  is actually { a<b }.

Can you give some bounds on what you expect the system to do?  For
example, Presburger arithmetic cannot (I believe) deal with x*x>y, just
2*x>y.
Does this matter to you?

And "deal" with is also kind of vague.  What you seem to what is an
algorithm that will find a  
unique, canonical, form for any inequality.  I think what the Omega
system, referred to in the URL from J.J.Green, can do, is some
transformations,
and probably has a proof system that will determine if a certain
expression
is a tautology.
 That is not the same as a system that will produce a
canonically simplified expression.
 
> >
> > I need to call the simplifier from within another program, i.e. I am
> > interested in a library of functions and not a human interface program.

There are programs (traditionally written in Lisp) that do some
canonical (e.g. polynomial simplification) and some heuristic
transformations that might be useful; perhaps more to your advantage
in Lisp is that the representation of such expressions is provided
in the language, which also uses that representation for programs.
e.g.  (and (< a b) (not (eq a b)))    as well as  (< a b)  are 
lisp expressions which could appear equally well in data or
programs.

> 
> Your problem concerns the Prusberger arithmetic, which is

Presburger actually.

> known to be (very) hard.

Hard in the sense of computation time.  I'm not sure the programs
are hard to write.  

> There is not a lot of code around,
> but you might look at the omega project
> 
>    http://www.cs.umd.edu/projects/omega/
> 
> I would be interesed to hear more on you application.
> 
> Cheers
> 
> Jim
> --
> J.J.Green, Dept. Applied Math. University of Sheffield, UK
> http://www.arbs.demon.co.uk

Good luck,
 Richard Fateman