Is anyone familiar with software that can mathematically solve problems? Not just the plain algebra\equation solving stuff, but really theorem driven reasoning.

I wonder.. would a similar approach be viable when it comes to software that is writing software? Formulate a problem in terms of math (?) or maybe a more domain-specific language and let a program create a solution for it.

---

Hapiness isn't hapiness without a violin playing goat

I guess the best that fits your demands is MATLAB (MATrix LABoratory).
I used it at uni and it is really great. It has a huge library and tons of webpages to find ways to solve special problems. Even if you only have the values and are looking for the solution.
But I think to remember me that it was really expensive

---

People have hope
Because they cannot see Death standing behind them.
-=Tite Kubo=-

Tyrkish:

I guess the best that fits your demands is MATLAB (MATrix LABoratory).

whatsInAname8:

theorem driven reasoning.

MATLAB doesn't do that. As far as I remember, MATLAB can almost only solve problems numerically. You'd get a lot further with Mathematica, which unfortunately also is not powerful enough – it can symbolically evaluate theorems you input to some extent (often needs some manual nudging in the right direction) but you can't have it find new appropriate theorems for some problem.

I don't know of any program that's so powerful ... it's an incredibly hard problem as well, obviously.

make your own, and do it using LOLCODE

---