Re: [Maxima-discuss] upper bound and lowerbound facts for declare

[Barton W. <wi...@un...>]

This is a bug:


  (%i2) fourier_elim((x>=-1 and x<=1) and x=0, [x]);
   (%o2) emptyset


If you could report it, that would be great.


Maxima's logical connectives aren't purely simplifying functions and are short- circuited.  Maybe I'm making excuses for myself (I wrote fourier_elim), but I think it's sometimes a bit difficult to support Maxima's logical connectives in such contexts.




--Barton
________________________________
From: Soegtrop, Michael <mic...@in...>
Sent: Thursday, March 9, 2017 10:01:07 AM
To: Barton Willis; Michel Talon; max...@li...
Subject: RE: [Maxima-discuss] upper bound and lowerbound facts for declare

Dear Barton,

I tested it a bit and it looks very interesting. It also supports and/or/not logical connections, so that it should be easy to map "follows b from a " questions to it. I have to think more about this and do some examples.

But I think it needs some testing/debugging. E.g. the below example seems to be wrong:

(%i2) fourier_elim((x>=-1 and x<=1) and x=0, [x]);
(%o2) emptyset

but (correct):

(%i5) fourier_elim([x>=-1, x<=1, x=0], [x]);
(%o5) [x=0]

Other logical connections I tried work fine, including not, which is not mentioned in the documentation, e.g.:

(%i7) fourier_elim(not x>=0,[x]);
(%o7) [x<0]

I guess I should go ahead and write some random test case generator, which verifies against Z3 or Coq.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de<http://www.intel.de>
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928