@asmeurer: Thank You for reviewing my proposal and suggesting changes.
It feels a bit like a laundry list. I realize that you don't really > know what is priority. I would rather focus the proposal. Some > thoughts on focus areas (depending on what interests you): > At this point even I think that my focus is diluted and I may have underestimated the time required for particular jobs. I will restructure my timeline to primarily work on 2 major things, SAT solver and FoL framework. The extra ideas, Semantic Tableaux and Inference Engine for FoL will probably have to take a step back (will add those to future ideas). - Implementation of first-order logic. If you want, you could focus on > monadic calculus (only one variable), which is more decidable than > full first-order logic. Take a look at what Maple and Mathematica have > implemented to get an idea of what is possible, and also what sort of > syntax to use. > I had a look at Mathematica (earlier) and Maple (now). The syntax I wish to implement is quite consistent with both their syntax. When I first imagined this project, I wanted SymPy to be able to do (atleast the basic) stuff that Prolog does (preferably with similar syntax). Focusing on monadic calculus will probably make the use scenarios for the module very concentrated. Additionally, going for a full FOPC will give a more academic approach to the module, wherein it can be used by institutions for demonstration of concepts and algorithms related to First Order Logic (which are not as intuitive as their propositional counterpart). I have been planning to add an optional step by step output for functions like conversion to normal forms and resolution. > I think a lot of what makes your proposal feel like a laundry list is > that some of your ideas are a single pull request, and some could be a > whole summer. For example, changing the printing of the logic > functions is easy; improving the SAT solver with ideas from minisat is > not. But both take up the same amount of space in your proposal. For > the ideas that are actual implementations of algorithms, you should > spend some time discussing their implementation, not just what they > are. > I perfectly understand the thing you are trying to say. The ironic thing is there is a perfect negative correlation between space on my proposal and time required to complete the job. I will add the implementation details to the major algorithms and try to condense the small tasks. Additionally I will tag each task depending on its size. I'm not sure I follow you here. Can you give a short example to show > what you mean in each case (integrated or not integrated)? > I like the idea given by @srjoglekar246 on the issue, and will go for the integrated version. "Ideally, we should have the FOL core running on the propositional logic framework. Having the same functionality in different forms in different places introduces redundancy and also the problem of changing code twice, if an enhancement has to be added." > As I noted on your proposal in Melange, what does "implementing > MiniSAT" mean? Do you intend to write Python bindings for MiniSAT (if > so, you should demonstrate to us that you know C++, and the Python C > API)? > > Or do you really mean, "improve the DPLL algorithm", which is already > in SymPy? There are some ideas for this at > > https://groups.google.com/forum/#!searchin/sympy/muise%7Csort:date/sympy/Cb_uhh3MuE4/k-hSQnxpyv4J > (the posts by Christian Muise in particular). > Analogous to my Melange reply, I mean improve the current algorithm to use the heuristics implemented in MiniSAT. After receiving this mail, I went into some heavy duty history hunting and went through all the posts by Muise on the mailing list as well as on his blog and have got a much better idea on what is already present and what more should be added. I will update the proposal to better describe my original ideas and some newly acquired ones. As noted above, I have underestimated the time required for the SAT solver. Even after working through the community bonding period on the solver, I will need more time to implement all the required features, test and benchmark the results. Will make changes to the timeline accordingly. Side Remark: Inspired from @haz's blog, I will add graphs to my pull requests to show the comparison between running time of all the algorithms. Well, no one wants to say "I'll be the mentor" for exactly that > reason, because then they'll get bugged more often :) > Thank You :) -- 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/CAGypG-O8t%2B7YgaauLy4mK2Fdap387nMtMMgy1a%2B6jDXxZEtWGQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
