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.
>>
>>
>