rtoy / maxima

A Clone of Maxima's repo
Other
0 stars 0 forks source link

logic_simplify handles inequalities incorrectly #1872

Open rtoy opened 4 months ago

rtoy commented 4 months ago

Imported from SourceForge on 2024-07-05 10:19:18 Created by robert_dodier on 2020-02-13 20:11:15 Original: https://sourceforge.net/p/maxima/bugs/3608


Function logic_simplify in the share package logic seems to handle inequalities incorrectly. In the second example I expected a and (b < 0) instead of true.

(%i1) load (logic) $

(%i2) logic_simplify (a or (not a) and b);
(%o2)                               a or b
(%i3) logic_simplify (a or (not a) and (b < 0));
(%o3)                                true

Working w/ Maxima 5.43.2 + SBCL 2.0.0 on MacOS.

rtoy commented 4 months ago

Imported from SourceForge on 2024-07-05 10:19:20 Created by philomath on 2020-02-17 17:52:19 Original: https://sourceforge.net/p/maxima/bugs/3608/#f060


Sir, I have worked on a bug fix on this issue and the fix is availabe at - https://sourceforge.net/u/philomath/maxima_translate/ci/logic_bug/tree/share/logic/

I have introduced a check on expression to be simplified if there is a subexpression depending on an unknown variable - (b < 0) - in the above example, and replaced it with a new variable interned using gensym. Then logic_simplify performs the simplification, and after that, all the interned variables are substituted back for the original expressions.

I have also added a few test cases to rtest_logic.mac

Kindly go through the changes.

rtoy commented 4 months ago

Imported from SourceForge on 2024-07-05 10:19:23 Created by philomath on 2020-02-18 10:14:55 Original: https://sourceforge.net/p/maxima/bugs/3608/#e45f


A further check that can be incorporated in above scheme is to check whether the subexpression being substituted by gensym is reducible to a logical True/False or not, for example:

  1. All subexpressions consisting of only relations operators (>, <, >=, <=, ==, etc.) are reducible to boolean values.
  2. Expressions like (a + b) may not be reducible to boolean values.

If the subexpression is not reducible to a boolean value, then an error like "Not a valid logical expression" could be reported. I am not sure about the possibility of detecting this though.

Kindly provide your suggestions.

rtoy commented 4 months ago

Imported from SourceForge on 2024-07-05 10:19:27 Created by robert_dodier on 2020-04-07 02:02:07 Original: https://sourceforge.net/p/maxima/bugs/3608/#7427


Hi Lakshya, sorry for the late reply. I think that triggering an error is too restrictive -- what if someone writes f(x) or g(y) for some unknown functions f and g? My advice is to just replace those with gensyms also.

rtoy commented 4 months ago

Imported from SourceForge on 2024-07-05 10:19:30 Created by philomath on 2020-04-08 18:02:46 Original: https://sourceforge.net/p/maxima/bugs/3608/#84ac


Thanks for the reply.

I had created a merge request with the gensym part which was merged. I think the issue has been resolved. Kindly let me know if there is any further work to be done.