SLD Resolution is sound and refutation-complete and it is the basis not only of Prolog but also the most successful bunch of SAT solving algorithms in the last, dunno, several decades.
"Very dumb theorem prover"!
-- Richard O'Keefe
SLD-Resolution is sound and refutation-complete (and also complete with subsumption). If you think that O'Keefe is right to say that it's a "very dumb theorem prover" then explain to me why _you_ think so, not who said it.
Because I, too, can quote you authorities- and probably bigger than O'Keefe.
I didn't remember that quote from O'Keefe. Prolog is indeed not trying to be smart and SLD-Resolution is dead simple - it's a sound and complete deductive inference system with a single rule. The reason Prolog is in turn so simple is because, thanks to the refutation-completeness of SLD-Resolution, you can implement it as a Depth-First Search for resolvents and then spam it until you get a result (or until you hit an infinite branch... oops). That's certainly orders of magnitude more simple than every other solver or automated theorem prover out there, like you say.
If that's what O'Keefe means, that Proolog is not trying to be smart, then OK, but that's not dumb. Every other solver tries to be smart and ends up having to solve an unsolvable problem. Who's dumb now then?
But maybe that's the compliment, I don't remember the context of O'Keefe's comment. Was it in the Craft of Prolog?
Now why would syntax be that important? It's because it directly enables homoiconicity, which is central to Prolog metaprogramming features: executing Prolog code returns a Prolog term, that can be reused. This is the distinctive characteristic of Prolog compared to more mainstream solvers, and what makes it 'a good programming language because it's a very dumb theorem prover'.