Assumption system and automatic theorem proving. Should I be learning LISP ?
This is the third time I attempt to write the assumption system. Other attempts could be described as me following the rule: “For any complex problem, there is always a solution that is simple, clear, and wrong.” My first attempt (although better than the current assumption system) did use very rudimentary logic and was not very smart. It could infer some basic rules, like Integer => Rational, but could not construct long paths like Prime => Integer => Rational => Real => Complex. You would have to specify by hand that prime numbers are also complex ... and this just what makes the old assumption system unmanageable. I know that state-of-the art CAS like Mathematica use advanced resolution techniques to get smart results. And in the open source world, well, the only CAS that I could find that has this sort of algorithms in Maxima, but in order to understand that I would have to learn LISP, and ironically enough I started to contribute to SymPy because I didn't feel like learning LISP ...