Not a bug, just simplemindedness. Sign is really quite stupid. Of course,
we'd be delighted if you'd work on improving it....
-s
On Apr 2, 2013 7:35 PM, "Mike Valenzuela" <mickle.mouse at gmail.com> wrote:
> Okay, I discovered some very strange behavior indicating that sign is not
> working correctly
>
> %i1) assume(zi <= vi+ni*ci, zi>=0, vi>=0, ni>=0, ci>=0)$
> %i2) sign( (zi-(vi+ni*ci)));
> %i3) sign(-(zi-(vi+ni*ci)));
>
> %o2) pnz
> %o3) pz
>
> This seems to indicate a bug. I suspect the problem lies in multi-term
> inequalities expressed in assume. I would guess that in the first case
> Maxima is performing the following:
> zi is pz,
> vi is pz,
> ni is pz and ci is pz, therefore ni*ci is pz
> pz - pz - pz is pnz.
>
> But when it reads vi+ni*ci - zi, I guess it matches correctly the whole
> term vi+ni*ci. If this problem is related to my suspicions, then there
> should be a priority given to larger terms or for the search to consider
> multiple branches rather than a single path. Following multiple branches
> also gives the opportunity to find contradictions in the assumptions.
>
> Alternatively, maybe there would be a way to test a hypothesis? Something
> like is( zi-(vi+ni*ci) <= 0 ). This would "narrow" the search to a
> simple proof.
>
> Along those same lines, Maxima could implement set-of-support-resolution
> (a strategy for http://en.wikipedia.org/wiki/Automated_theorem_proving) for
> simple proofs. I'm not sure how large the database would need to be to
> cover sign logic (and before someone mentions Godel's incompleteness
> theorem, I know that some true statements must be unprovable, the logic
> must have an infinite number of axioms, or the logic must be inconsistent).
> If someone felt so inclined, the automated prover could be extended to
> other simple logic.
>
>
>
> On Tue, Apr 2, 2013 at 4:11 PM, Mike Valenzuela <mickle.mouse at gmail.com>wrote:
>
>> Earlier I typo'ed, I meant sign(zi - vi - ni*ci) should clearly be "nz"
>>
>>
>>
>> On Tue, Apr 2, 2013 at 4:09 PM, Mike Valenzuela <mickle.mouse at gmail.com>wrote:
>>
>>> Hello,
>>>
>>> I am attempting to determine the sign of an expression, but I have
>>> discovered that sign fails to solve even simpler problems than I am working
>>> on.
>>>
>>> %i1) assume(zi <= vi+ni*ci, zi>=0, vi>=0, ni>=0, ci>=0)$
>>> %i2) sign(zi - vi - ni*ci);
>>> %o2) pnz
>>>
>>> In my mind the answer seems to clearly be pz.
>>> Following from:
>>> zi <= vi+ni*ci
>>> zi -(vi+ni*ci) <= 0
>>> zi -vi - ni*ci <= 0
>>>
>>> I'm not sure if there is another package I have to include or what other
>>> assumptions are needed. Maybe the sign function is incomplete? Maybe
>>> inequalities are harder for Maxima to work with than equations?
>>>
>>> BTW, I'm using maxima version 5.28.0-2.
>>>
>>>
>>
>
> _______________________________________________
> Maxima mailing list
> Maxima at math.utexas.edu
> http://www.math.utexas.edu/mailman/listinfo/maxima
>
>