On Wednesday, March 12, 2014 3:54:02 AM UTC+5:30, Soumya Biswas 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. > > 1. 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. > > Ideally, we should have the FOL core running on the propositional logic framework. Like in a prenex normal form, the relevant terms can be replaced with dummy Symbols and then solved using a propositional KB. Things like cnf conversion are better kept just in one module, and reused - though it _may_ mean a little complex code. 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.
> > 1. 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). > > I would suggest you add your code to sympy.logic module, and then later (after GSoC) try to update the assumptions system with the functionality. Trying to do it the other way round may make the overall system quite inconsistent and messy in the intermediate stages of your work - it may prove difficult to come out of it (my thoughts). > > 1. 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. > > +1 to that. You can keep both the solvers in the module, and use the 'faster' one for the default SAT solving in sympy. > > 1. > 2. 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. > > @asmeurer would be a better person to comment on this. Though for now you should probably focus on the work you have previously proposed (your proposal should make things clearer). Once Aaron has a look at the proposal, you guys can think of how your code will help the assumptions module. > > 1. 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. > > 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 [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/72fe94ff-7844-42cf-8d77-e0f2bf40df7f%40googlegroups.com. For more options, visit https://groups.google.com/d/optout.
