Re: Should facts() show duplicate facts?

Yes, CAD implementation would be nice. But ...

   - The best is the enemy of the good.
   - Who will bell the cat?

Fixing the many bugs in the existing system is a Good Thing, and I'm very
thankful that David Scherfgen has undertaken the task (with AI help).

What's more, many of the bugs he's addressing are orthogonal to the
qualities of CAD. They're about maintaining the database of facts, not
about making inferences based on those facts.

On Thu, Aug 27, 2026 at 4:39 PM Richard J. FATEMAN via Maxima-discuss <
[email protected]> wrote:

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

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