I don't understand what CAD has to do with the problem. It could be
used to verify a theorem like "If a!=0, then x>y iff (a>0 and a*x>a*y)
or (a<0 and a*x<a*y)", but that doesn't help us decide how to
represent and print a*(x>y).
sage: qepcad('[a /= 0 ==> [x > y <==> [ [a x > a y /\ a > 0] \/ [a x <
a y /\ a < 0] ] ] ]', vars=('a','x','y'))
TRUE
> Carl Witty has (unreleased) Sage code for doing such things. We also
> have an optional spkg for qepcadb, which computes such things.
>
> Unfortunately, it seems like Carl has not been active in the project
> lately, so I don't know who else could or wants to do this. Carl: if
> you are reading these messages, is there the possibility you could post
> your code somewhere so interested people could work from there?
I'm back to being active. If there are people interested in
half-written, slow CAD code I'd be happy to work with them! My
impression, though, was that there were a few people interested in
having my work in Sage, but nobody interested in actually helping me
write the code. (Which is fine, it just means it'll take a while to
get finished.)
> I might note that Mathematica has a very powerful CAD implementation,
> from what I understand.
>
> Jason
Carl