Hi, I am Luv Agarwal, a sophomore pursuing b-tech in computer science. From the past 20 days I have been hopping around CAD (cylindrical algebraic decomposition) and Quantifier Elimination basics, algorithms, improvements and other related stuff to successfully and efficiently implement it. Other than these I read about other uses of CAD like Inequalities solving, collision detection which I suppose can be implemented in the course of Quantifier elimination implementation.
It will be really good if SymPy can perform CAD as it can then be used for quantifier elimination, theorem proving in algebraic geometry, evaluating multiple integrals and in assumptions engine. (Source: https://mattpap.github.io/masters-thesis/html/src/conclusions.html#cylindrical-algebraic-decomposition ) I Plan to implement *partial cylindrical algebraic decomposition and quantifier elimination* (By - George E. Collins and Hoon Hong). I will check if this *partial CAD *can be used in other CAD applications. If not then I will make sure that I think of an implementation which can perform both partial as well as full CAD. *My current status of quantifier elimination:* I have read the following: 1. Collin's original paper *Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition* which contains the core algorithms. 2. Few papers which talk about the usage of CAD. 3. Hong's implementation of quantifier elimination from partial cylindrical algebraic decomposition that introduces *partial cad *which is an enhancement of the complete CAD to perform quantifier elimination. 4. A small but powerful improvement By Hong in a CAD projection operator. After all this heavy reading I have a good understanding about the working of these algorithms and what will be needed to implement it. (I have implemented a small component (projection phase) of CAD for testing purposes). Though I haven't thought about it's implementation details in SymPy, but I have thought in general. I will soon post those details together with my GSoC proposal. Also, can someone please update me why FOL (GsoC-2014 by Soumya Dipti Biswas) is not yet merged as quantifier elimination demands it. Algorithm Functionality: Input: A quantified formula F. Output: A quantifier free formula F' (in free variables of F) equivalent to F. Example: >>> F = ForAll(x, x*y=0) >>> Reduce(F) >>> y = 0 It would be a great help if I can get some community feedbacks. Thanks. -- 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 post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sympy. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/440e0d91-c457-457e-9c1f-2e22832e5e23%40googlegroups.com. For more options, visit https://groups.google.com/d/optout.
