Comment by gems
13 years ago
The only thing I asserted in that comment was that you can't ask the computer to help you (effectively) in a naive search when the space is large or infinite. I'm not familiar with how theorem provers work, so I'm most likely wrong anyway.
How does a computer build abstractions on its own?
How does it build them? That's not a simple question, but it's possible to do. E.g. machine learning is computers building abstractions.
But it doesn't have to do that, anyway, it can provide means for users to build their own abstractions, abstractions that may be useful for them.