>> Prolog is really for indeterministically searching a large/infinite space such as in planning (and yes it can be used for theorem proving and program verification as well).
I'd say theorem proving is what Prolog "is really for", in the sense that it's a language whose interpreter is an automated theorem prover.
It just so happens that a (first-order) theorem prover is the best tool to explore an infinite space, if it's worth its salt, because that's what it has to do in order to find a proof in the first place.
And of course you can cast all sorts of combinatorial problems like planning and verification as proofs (this sequence of actions reaches this goal state from this starting state).
Edit: incidentally, it's so dumb that the standard for pattern matching in the industry is regexes, with their insufferable, cryptic pandemonium of notations, rather than Prolog, which has got to be the language with the simplest possible syntax in all of computer science this side of Brainfuck. When I was doing my NLP homerwork during my MSc I kept writing small ad-hoc parsers that were all balls of mud around a bunch of regex scripts, and I longed for the simplicity of Prolog and its DCGs (I couldn't use Prolog because the homework was in Python and at the time there was no Janus). Why do programmers do that to themselves?
I'd say theorem proving is what Prolog "is really for", in the sense that it's a language whose interpreter is an automated theorem prover.
It just so happens that a (first-order) theorem prover is the best tool to explore an infinite space, if it's worth its salt, because that's what it has to do in order to find a proof in the first place.
And of course you can cast all sorts of combinatorial problems like planning and verification as proofs (this sequence of actions reaches this goal state from this starting state).
Edit: incidentally, it's so dumb that the standard for pattern matching in the industry is regexes, with their insufferable, cryptic pandemonium of notations, rather than Prolog, which has got to be the language with the simplest possible syntax in all of computer science this side of Brainfuck. When I was doing my NLP homerwork during my MSc I kept writing small ad-hoc parsers that were all balls of mud around a bunch of regex scripts, and I longed for the simplicity of Prolog and its DCGs (I couldn't use Prolog because the homework was in Python and at the time there was no Janus). Why do programmers do that to themselves?