Re: Should facts() show duplicate facts?

I think that addressing the creation and querying of a 'database of
algebraic inequalities'
may require an implementation of a system we have avoided for decades, but
has been the topic of discussion in some other systems. Cylindrical
algebraic decomposition would allow a program to determine, given a set of
(algebraic) equations defining a region, whether a point is inside that
region.  This doesn't address log, exp, etc functions.
The 'assume' database works for very simple cases, but I think 'debugging'
it is not going to address serious shortcomings.
see https://en.wikipedia.org/wiki/Cylindrical_algebraic_decomposition
You might read that CAD
 is Fundamental to CAS,  which of course makes one wonder how we've done
without it.
Read the wikipedia article and some references.
  One issue is that -- whatever it is you want to do with CAD, it comes
with a cost, namely the algorithms are generally doubly-exponential in the
number of variables.  The interest in it (by G.E.Collins) was sparked by
finding an alternative for Tarski's decision procedure.
RJF

On Thu, Aug 27, 2026 at 6:56 AM David Scherfgen via Maxima-discuss <
[email protected]> wrote:

> I found this while working on bug #5120, and it surprised me, so I suspect
> it will surprise others too: The fact database can hold the same fact more
> than once, and facts() does not tell you.
>
> assume(notequal(a, 0))$
> assume(notequal(a*b, 0))$
> facts();
>   [notequal(a, 0), notequal(b, 0)]
>
> forget(notequal(a, 0))$
> facts();
>   [notequal(a, 0), notequal(b, 0)]
>
> The fact notequal(a, 0) existed twice, but facts() shows it only once. One
> must call forget() twice for the fact to actually disappear.
>
> The reason is that some assumptions are filed as several facts.
> notequal(a*b, 0) is stored as notequal(a, 0) together with notequal(b, 0),
> because that is the form the database can actually answer questions from.
> These internal facts are stored even if the database already contained
> them. On the other hand, trying to establish the same fact twice using the
> user-level function assume() will answer [redundant] from the second time
> on.
>
> That second copy of the fact is not a bug, and I want to be clear about
> that, because my first instinct was to call it a bug. It works as a "count
> of reasons", and it is what makes this case come out right:
>
> assume(notequal(a*b, 0))$
> assume(notequal(a*c, 0))$
> forget(notequal(a*b, 0))$
> facts();
>   [notequal(a, 0), notequal(c, 0)]
>
> notequal(a, 0) correctly survives, because notequal(a*c, 0) still says so.
> If the two assumptions shared a single entry, that forget would have taken
> it away.
>
> The one thing that does seem wrong is facts() not showing the duplicate
> facts, and because it is the only window users have, the whole thing looks
> inconsistent: forget() says it removed something, but then facts() says it
> is still there. And forget(facts()) doesn't work as one might reasonably
> expect.
>
> My proposal is simply that facts() should stop suppressing duplicates.
> forget(facts()) then becomes exact, and facts() agrees with what forget was
> already reporting.
>
> Duplicates appear only where there genuinely are two independent reasons
> for the same statement, which is exactly the situation a user needs to know
> about.
>
> This doesn't cause any test failures. But it is a user-visible change, so
> it would want a line in the manual saying a statement can appear more than
> once when more than one assumption supports it. It changes nothing about
> what assume means or what the database stores, only about what you are
> allowed to see.
>
> Is anyone opposed, or relying on facts() returning each fact at most once?
>
> There is a larger question behind this about whether the database should
> record what the user said or what Maxima knows, and the counting above is
> an approximation of the former. I would rather leave that for another
> thread and just stop hiding the count.
>
> Best regards
> David Scherfgen
> _______________________________________________
> Maxima-discuss mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/maxima-discuss
>

_______________________________________________
Maxima-discuss mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/maxima-discuss