You might enjoy ruler https://github.com/uwplse/ruler https://github.com/uwplse/ruler It would be very interesting for SMT and CAS to converge a bit more. SMT

You might enjoy ruler https://github.com/uwplse/ruler https://github.com/uwplse/ruler It would be very interesting for SMT and CAS to converge a bit more. SMT in expressiveness and domains and CAS in rigor. The modality of their usage is different. CAS tends to return some expressions of interest, which it is hard to get SMT to do. Either you get "unsat" or a particular model from an SMT solver, not a simplified expression (ok, z3 has a simplify command, which is pretty cool). SMT today is not obviously expressive enough to handle most of the domains and questions that come up in CAS systems. Most SMT solvers do not intrinsically handle transcendental functions or any notions of calculus, abstract algebra, etc. CAS systems are largely interested in problems of equational reasoning, whereas SMT's bread and butter is gluing together "trivialities" like linear inequalities and congruence closure with SAT search.