Hi Stavros,
Thanks for the code.
I called it 'sdiff.lisp'
Here is what I get.
(%i1) load("sdiff");
(%o1) ./sdiff.lisp
(%i2) assume(x > 2);
(%o2) [x > 2]
(%i3) is (x^2 > 3);
(%o3) true
(%i4) is (x^3 > 7);
(%o4) true
(%i5) assume(y < 3);
(%o5) [y < 3]
(%i6) is (y < x^2);
(%o6) unknown
So, it solves the immediate problem of x^2 > 3, but not one in which
one adds other variables.
Actually, what would really be nice is to have an 'inequality solver'
which works at least for several linear, quadratic, and cubic polynomial inequalities
(and, OK, quartic, too!).
I realize that this may be a low priority, but does it at least seem
possible?
TIA,
-sen
On Tue, 5 Jun 2007, Stavros Macrakis wrote:
> I *did* attach the file, but for some reason it is not appearing -- gmail
> glitch?
>
> Anyway, here it is in line:
>
> (defun signdiff-special (xlhs xrhs)
> (when (or (and (numberp xrhs) (minusp xrhs)
> (not (atom xlhs)) (eq (sign* xlhs) '$pos))
> ; e.g. sign(a^3+%pi-1) where a>0
> (and (mexptp xlhs)
> ;; e.g. sign(%e^x-1) where x>0
> (eq (sign* (caddr xlhs)) '$pos)
> (or (and
> ;; Q^Rpos - S, S<=1, Q>1
> (memq (sign* (sub 1 xrhs)) '($pos $zero $pz))
> (eq (sign* (sub (cadr xlhs) 1)) '$pos))
> (and
> ;; Qpos ^ Rpos - Spos => Qpos - Spos^(1/Rpos)
> (eq (sign* (cadr xlhs)) '$pos)
> (eq (sign* xrhs) '$pos)
> (eq (sign* (sub (cadr xlhs)
> (power xrhs (div 1 (caddr xlhs)))))
> '$pos))))
> (and (mexptp xlhs) (mexptp xrhs)
> ;; Q^R - Q^T, Q>1, (R-T) > 0
> ;; e.g. sign(2^x-2^y) where x>y
> (alike1 (cadr xlhs) (cadr xrhs))
> (eq (sign* (sub (cadr xlhs) 1)) '$pos)
> (eq (sign* (sub (caddr xlhs) (caddr xrhs))) '$pos)))
> (setq sign '$pos minus nil odds nil evens nil)
> t)
> )
>
--
---------------------------------------------------------------------------
| Sheldon E. Newhouse | e-mail: sen1 at math.msu.edu |
| Mathematics Department | |
| Michigan State University | telephone: 517-355-9684 |
| E. Lansing, MI 48824-1027 USA | FAX: 517-432-1562 |
---------------------------------------------------------------------------