[AnaniasAnanas]

Prolog is Turing-complete, you can have non-terminating programs in it (and thus there are problems that can be expressed in Prolog that you can never get an answer to), does the same hold true for Alloy? If not I think that it would make more sense to compare Datalog (which I think forces all of its programs to provably terminate) with Alloy rather than Prolog with Alloy.

[hwayne]

Alloy forces you to bound all of your models, so it will always terminate.