I think you should go into more details with the quantifiers. Second order formulas can quickly get you into the realm of undecidable problems. Also some quantifier elimination algorithms are complex (for instance, CAD, which is one of the other GSoC idea projects, is a quantifier elimination algorithm). I would just start with getting the basic symbolic implemented, and maybe implement some simple deductions on them. The inability to symbolically represent quantifiers in SymPy's logic system has never been an issue, which is why they haven't been implemented yet. But it would be useful to have them. You should also look at other systems such as Sage, Z3, Maple, Mathematica, and other systems to see how they implement quantifiers and what sorts of operations they support.
Alternatively, if you want to deemphasize the quantifier part of your application and emphasize the algorithmic improvement parts instead, that would also be fine. The algorithmic improvements are more important than implementing quantifiers. Symbolic quantifiers would be nice, but as I've noted part of the reason they've never been implemented is that we haven't needed them. The main benefit they would provide to the assumptions would be the ability to represent certain types of facts in a more compact way. Aaron Meurer On Thu, Apr 3, 2025 at 2:58 PM Krishnav Bajoria <[email protected]> wrote: > Hello everyone, > I have made some more changes to the timeline in my proposal. Please > review it here > <https://drive.google.com/file/d/1gVxdNcVZsXlxrflNs0UPN5W3cbA7NLhN/view> > and let me know what you think. If there is anything anyone would like me > to change I would be happy to do so. > Also to Tilo, I understand that PR was more to deepen my understanding and > have a look through/glance rather than a thorough review. > Best regards, > Krishnav Bajoria. > > On Thu, Apr 3, 2025 at 10:02 PM Tilo RC <[email protected]> wrote: > >> Don’t review it thoroughly. I don’t expect you to understand it. I just >> wanted you to know it exists. >> >> On Thu, Apr 3, 2025 at 1:10 AM Krishnav Bajoria < >> [email protected]> wrote: >> >>> Hello Tilo, >>> >>> I've been analyzing that PR since you pushed it. Given the size of the >>> code, it's taking some time to review it thoroughly, but I'll get back to >>> you once I've gone through it completely. >>> >>> Thanks again for pointing me to another valuable PR—it's been helpful >>> for my understanding of SAT/SMT solvers. >>> >>> Best Regards, >>> >>> >>> Krishnav Bajoria. >>> >>> -- >>> You received this message because you are subscribed to a topic in the >>> Google Groups "sympy" group. >>> To unsubscribe from this topic, visit >>> https://groups.google.com/d/topic/sympy/XSJuvibPOro/unsubscribe. >>> To unsubscribe from this group and all its topics, send an email to >>> [email protected]. >>> To view this discussion visit >>> https://groups.google.com/d/msgid/sympy/CAF0TZuvvJFtxLnQ%3D_1HDwfKnAx0VKkpLzm_hON4AERUDcnL9zw%40mail.gmail.com >>> <https://groups.google.com/d/msgid/sympy/CAF0TZuvvJFtxLnQ%3D_1HDwfKnAx0VKkpLzm_hON4AERUDcnL9zw%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "sympy" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion visit >> https://groups.google.com/d/msgid/sympy/CAEgDm30cguwMTDYiUwzD1sBY4PZxGQzKGz%3DX%3DCEzsKMEj8QUgA%40mail.gmail.com >> <https://groups.google.com/d/msgid/sympy/CAEgDm30cguwMTDYiUwzD1sBY4PZxGQzKGz%3DX%3DCEzsKMEj8QUgA%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/sympy/CAF0TZusUYieF4s-DJJNPGLnrvz2LrLhrEZnPR%2BpGo55JVKn2GQ%40mail.gmail.com > <https://groups.google.com/d/msgid/sympy/CAF0TZusUYieF4s-DJJNPGLnrvz2LrLhrEZnPR%2BpGo55JVKn2GQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6KY6xndetrqCshJ2QuipUU5S5iUfAT-iG1TefuU3hpBRA%40mail.gmail.com.
