First post on my GSOC adventure. This year I got accepted in Google's summer of code program as student, and my job will be to implement the assumptions framework in SymPy. Although the project officially is only about implementing an assumptions framework, I have to prepare the ground before the official start of the program so that I can finish in time. Basically, this means refactoring the logic module, as this is the foundation of the assumption system. Current logic module was written with the old assumption system in mind, and has done a great job with that, but has some limitations: - Non-standard API. From what I've read, everybody is calling the knowledge base KB, whereas we call it FactRules. Ask method is normally called Ask(), but we call it deduce_all_facts(), etc. - Does not implement backward chaining, and I really need backward-chaining to make the assumption system a bit smart. - No support for first-order logic, only propositional logic This is a must for anyone doing serious work in logic. - Seems over complex. This is only an impression, but I've read other logic modules (aima-python), and they are much easier to understand. Books I am reading on the topic: - AI: A modern approach, Rusell & norvig - Combinatorial Theory, Martin Aigner (has some useful info about graphs)