Sorry for not responding sooner. This thread must have fallen through the cracks.
I've answered your questions inline. Let me just comment on the proposal itself here. 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): - 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. - Improvements to the SAT solver (see below for a link to some ideas) - Implement some other kind of "solver" like clause learning, truth maintenance system, etc. You should put priority on the sorts of things that would benefit the assumptions. 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 would try to clean it up, writing more about the hard things and less about the easy things. Otherwise, it comes off as if you don't really have a good idea of how difficult things are. Maybe you could make a more extensive full TODO list on the wiki somewhere that includes everything, easy or hard. On Tue, Mar 11, 2014 at 5:24 PM, Soumya Biswas <sdb1...@gmail.com> wrote: > I have almost completed my GSoC proposal on extending the propositional > knowledge base and creating a new module for first order logic. However > there are a couple of doubts that I would like to clear before putting up > the proposal online. > > Will first order logic be integrated with its propositional counterpart or > exist independently? Going for integration will make the code messy as > appropriate checks will have to be made at EVERY point. On the other hand, > independent existence will introduce a good amount of redundancy. 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)? > Many concepts from first order logic are implemented in the assumption > system (for e.g. predicates). However these implementations seem (I am not > sure if they are) to be quite specific in nature. Should I try to make > changes to the pre-existing code and build the rest of the codebase around > it? Right now my proposal involves building a generic first order logic > module from scratch. Additionally, once the logic module is mature enough to > handle the requirements of the assumption system, would the new assumption > use the new sympy.logic or continue to use the code in sympy.core / > sympy.assumptions (which seems to fulfill the need except for efficiency > parameters). This is unclear at this point. Currently, the code in facts.py is quite fast. It's possible that we may want several "cores" for the assumptions system, a fast but less powerful one and a slower but more powerful one. > One of my ideas is to create a faster SAT solver. Picosat and minisat appear > to be good candidates. As suggested by @asmeurer we could always use > something on the lines of pycosat (without making it a hard dependency) but > the native solver should still be as fast as possible. Currently I am > inclined towards implementing minisat (as pycosat can be used for picosat). > Some suggestion for an appropriate solver would be helpful. Is it mandatory > for me to declare the solver I am going to use in my proposal? I believe > this decision can only be taken after actual implementation and thorough > benchmarking. 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). > Considering that the assumption system is supposed to use the logic module > heavily, some indication about the functions required (by the assumption > system from the logic module) would be an enormous help. Anything you can think of can probably be useful. If you can imagine a mathematical fact that can be expressed and queried about in the assumptions system that would use the given logic, that is a use-case. With that being said, the most important stuff is already implemented. It just needs to be improved to be more efficient, and to better be able to handle things like efficient conversion to cnf. > If my proposal were to get selected, who would be the potential mentor? > A.K.A who am I supposed to bug for the next couple of days for suggestions > and improvements. There are some implementation issues that I really want to > discuss and put in the final proposal. Well, no one wants to say "I'll be the mentor" for exactly that reason, because then they'll get bugged more often :) > > Thanks in advance for the help. > > -- > 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 sympy+unsubscr...@googlegroups.com. > To post to this group, send email to sympy@googlegroups.com. > 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/3ab02e25-4ec7-4cfb-a696-e0fef118a25e%40googlegroups.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 sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. 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%3D6LNfg7RZWUcSrw4gTAcevLmaHX%2BEZS0Ut2ajMh%2Bi1cvuA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
