Having a look at pylog, it seems to be a small prolog engine and a limited subset of first order logic (FOL) -- no quantification for example. I wouldn't hope to re-invent things, but if sympy is to reason with a richer form of logics, then FOL is a natural next step. However, the point of starting this thread was to find a reasonable issue to patch as part of my application to SoC'10. Implementing an entire FOL reasoning engine (using pylog or not) seems slightly out of the scope of this goal :p.
@Fabian: Can you clarify how the use of FOL would simplify the assumption system? (ie. did you mean sympy's core assumption system (something I haven't fully grok'd yet) or the inference code in the logic module?) @Alan: My licensing chops are a bit rusty so I may be off, but since we would want to add / modify code that pylog provides (it's not clear that a straight hook in is possible), and since pylog is licensed under LGPL, we would have to roll our own implementation from scratch. On the other hand, it looks like there is only one copyright holder, and as such he should be able to re-license the latest version as BSD for a fork (it's worked for me in the past with other library licensing issues). So other than a new logic engine for sympy, are there any other obvious low hanging fruit I can get my hands dirty with? Cheers, Christian On Thu, Mar 18, 2010 at 7:32 AM, Alan Bromborsky <[email protected]>wrote: > Fabian Pedregosa wrote: > >> Mateusz Paprocki wrote: >> >>> Hi, >>> >>> On Wed, Mar 17, 2010 at 08:25:15AM -0700, Christian Muise wrote: >>> >>>> Having dug deeper, it appears that first order logic isn't even >>>> included in the current version of sympy. Is there some manner of >>>> generic (existential and universal) quantification in the sympy core >>>> that I'm missing? >>>> >>>> >>> there is no currently, so it might be one of your objectives to >>> implement them. >>> >> >> Indeed, I implemented the logic system using only propositional logic, >> but implementing first-order logic would simplify a lot the assumption >> system >> >> >>> Thanks. Cheers >>>> >>>> On Mar 16, 1:37 pm, Christian Muise <[email protected]> wrote: >>>> >>>>> I'm not sure what the procedure of cylindrical algebraic decomposition >>>>> is, >>>>> and I'm likely not suited for the topic of quantification in complex >>>>> algebras, polynomials, etc. But as far as quantifier elimination stands >>>>> for >>>>> boolean logic (alahttp://en.wikipedia.org/wiki/Quantifier_elimination), >>>>> I >>>>> can definitely put together the code for that. >>>>> >>>>> Is it not too artificial to create an issue (that's not exactly a bug, >>>>> but >>>>> a feature request), and then resolve it in order to strengthen a SoC >>>>> application? I definitely have a number of ideas for larger scale >>>>> projects >>>>> that may fit the SoC timeline nicely, but I'm coming up short for >>>>> immediate >>>>> issues as part of the application phase. >>>>> >>>>> Thanks for the reply and info. Cheers >>>>> >>>>> Christian >>>>> >>>>> On Tue, Mar 16, 2010 at 1:15 PM, Mateusz Paprocki <[email protected]> >>>>> wrote: >>>>> >>>>>> Hi, >>>>>> On Tue, Mar 16, 2010 at 07:24:19AM -0700, Christian Muise wrote: >>>>>> >>>>>>> Hello, >>>>>>> I was interested in applying for SoC this year, and as such I went >>>>>>> looking for issues to work on as part of the application process. >>>>>>> However, my main interest is primarily in logic, ie. anything that >>>>>>> goes under here: >>>>>>> -http://tinyurl.com/ylxkjdy >>>>>>> Issue 1545 is the only relevant looking one ( >>>>>>> http://code.google.com/p/sympy/issues/detail?id=1545), but I don't >>>>>>> want to step on the toes of Fabian or Ronan. Are there any other >>>>>>> options, or issues that I'm missing? >>>>>>> >>>>>> maybe you can consider working on quantifier elimination and >>>>>> cylindrical >>>>>> algebraic decomposition, see >>>>>> http://reference.wolfram.com/mathematica/tutorial/Quantifiers.html >>>>>> (for example). Of course you're free to propose something else, which >>>>>> matches your preferences more precisely. >>>>>> >>>>>>> Cheers >>>>>>> -- >>>>>>> You received this message because you are subscribed to the Google >>>>>>> Groups >>>>>>> >>>>>> "sympy" group. >>>>>> >>>>>>> To post to this group, send email to [email protected]. >>>>>>> To unsubscribe from this group, send email to >>>>>>> >>>>>> [email protected]<sympy%[email protected]>< >>>>>> sympy%[email protected]<sympy%[email protected]> >>>>>> >. >>>>>> >>>>>>> For more options, visit this group at >>>>>>> >>>>>> http://groups.google.com/group/sympy?hl=en. >>>>>> -- >>>>>> Mateusz >>>>>> >>>>> >>>>> -- >>>> You received this message because you are subscribed to the Google >>>> Groups "sympy" group. >>>> To post to this group, send email to [email protected]. >>>> To unsubscribe from this group, send email to >>>> [email protected]<sympy%[email protected]> >>>> . >>>> For more options, visit this group at >>>> http://groups.google.com/group/sympy?hl=en. >>>> >>>> >>> >> >> Should we make sure we are not reinventing the wheel - > http://christophe.delord.free.fr/pylog/index.html > > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To post to this group, send email to [email protected]. > To unsubscribe from this group, send email to > [email protected] <sympy%[email protected]>. > For more options, visit this group at > http://groups.google.com/group/sympy?hl=en. > > -- You received this message because you are subscribed to the Google Groups "sympy" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
