On Mon, Mar 17, 2014 at 6:37 PM, Soumya Biswas <[email protected]> wrote: > @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."
I'm still not really clear how a non-integrated version would work, but I'm glad you decided on an integrated one (which seems like the obvious way to do it to me). > >> >> 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. That's good. Improving the SAT solver alone could be a GSoC project. Aaron Meurer > >> 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. -- 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/CAKgW%3D6KtUGcaNX3kS39VQZXfEB30hCEE5bNaC%3D-SMtLaN8CLTQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
