(I'm no expert but..) I recently got into Prolog, and Alloy sounds very similar. So I was asking "How is it different?" Strangely, in the FAQ, no mention of Prolog. I found just this:
>How does the Alloy Analyzer differ from theorem provers?
>The Alloy Analyzer's analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It's a "refuter" rather than a "prover".
(i.e. where Prolog would just write "no" if nothing found.) In the Alloy* paper also, no mention of Prolog. To find a counterexample, couldn't you set Prolog to find one?
Prolog is a general programming language with built-in backchaining semantics. It in general does not know how to solve constraints. Indeed if your clauses have loops Prolog will just run in circles until it is out of stack space. The following common rules for equivalence are good examples of valid logic statements that do not work with Prolog's naive execution strategy:
% Symmetry
f(A, B) :- f(B, A).
% Transitivity
f(A, C) :- f(A, B), f(B, C).
Indeed in general finding the symmetric/transitive closure of relations is a very hard problem. Constraint/SAT solvers use heuristics to solve problems like the above and can accept much more declarative specifications than Prolog.
You could try in Prolog. But the other difference is that prolog is. General purpose language (though used in a more specific set of situations). Alloy is not.
Also the search mechanisms are not the same. Prolog uses a backtracking, depth-first search behind the scenes. Alloy does not.
EDIT: I was out earlier and didn't want to make a claim I couldn't verify/backup. Alloy uses a SAT solver behind the scenes to find solutions.
Alloy is a specification language. To verify the specification, the alloy analyser (a model checker) has to artificially create some number of instances and simulate it.
Prolog is an executable language. You, the user, give it a database, and it searches for solutions that satisfies constraints. It doesn't create the basic facts on its own.
There exists a compiler from imperative alloy to prolog to make this transition.
Hmm well, not all Prolog uses fit the 'give it a database' model..(In fact I can't think of any Prolog programs I've seen that do fit it) e.g. I was tried the the finite domain solver in Gnu Prolog[0] recently, I wanted arrangements of about 15 shapes that obeyed certain constraints, the program was 6 very short lines! I didn't tell it anything except the constraints.
But yeah, alloy and alloy* sound fascinating, I must investigate further, thank you.
You are right. Constraint solving in general is a specific area that does not require a knowledge base; instead it is a search for a solution from the specified domain that fits all the specified constraints. Here there is considerable overlap between prolog, alloy and z3.
However, most general prolog programming has the same requirements placed on other executable languages, to transform, store and communicate data. Alloy is not the tool for this aspect.
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.
>How does the Alloy Analyzer differ from theorem provers?
>The Alloy Analyzer's analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It's a "refuter" rather than a "prover".
(i.e. where Prolog would just write "no" if nothing found.) In the Alloy* paper also, no mention of Prolog. To find a counterexample, couldn't you set Prolog to find one?