[YeGoblynQueenne]

>> Constraint programming was much more like an AI to me than any actual AI, since I just described the constraints and my programs solved itself.

Theorem proving and SAT solving are classic AI subjects, don't forget. If we don't think of them this way today that's the usual "if it works, it's not AI" paradox (it's got a name I think, but I don't remember it).

I'd go as far as to say that theorem proving is honest-to-god AI, much more so than pattern recognition. After all, we know many animals that can recognise sights and sounds, but we only know of one animal that can state and prove theorems.