At a superficial level, it looks a bit like Z3, which I do have some experience with, but I suspect that there's a lot of intricacies to Prolog that don't apply to Z3.
Sadly non-'pure' logical programming is required to get real-world performance (eg. cuts that prune the search tree) which kind of feel like, or is, a leaky abstraction that breaks the magic.
I have had good success in solving logical problems by asking o1 to produce prolog programs.
I learnt Prolog a long time ago and would like to start from scratch.
They aren’t required but are convenient. Excuse brutalizing syntax and formatting but in Prolog you can do:
A(X) :- between(1,3,X).
B(X) :- between(1,1000,X).
?- A(X), B(X).
?- B(X), A(X).
Also cuts and pruning long time ago felt like bloated terms (when I didn’t get Prolog) whereas it’s a simple break equivalent in imperative languages loops.
SWI Prolog has great libraries, BTW.
https://web.archive.org/web/20040603192757/research.microsof...
You only get in trouble with the cut when you're just starting out and don't know what you're doing, and write your code in a way that it keeps entering infinite recursion or backtracking until the cows come home. At that point, because you don't yet know how to control those behaviours, you start sowing your code with cuts all over the place, which maybe stops the backtracking and infinite recursion (but maybe not) but it makes it an incomprehensible mess that still doesn't do what you want it to do.
As you grow and learn, you figure out how to control backtracking and recursion by ordering your program clauses and your clause literals in a sensible manner. At that point the use of the cut becomes so regular and formulaic that it might as well be added in by a pre-procesor.
For instance, you want a program that walks over a list and modifies an element if a condition holds, otherwise it continues, until the list is empty. You write:
% Program "skeleton" not meant to be executed but to expose a pattern
modify_list([],Xs,Xs):-
! % We're done, stop trying
modify_list([X|Xs],[Y|Acc],Bind):-
modify_element(X,Y)
,! Don't re-process X!
,modify_list(Xs,Acc,Bind).
modify_list([_X|Xs],Acc,Bind):-
modify_list(Xs,Acc,Bind).
I have relied heavily on both Z3 and Alloy for ad-hoc jobs, and Prolog doesn't even come close to the inference power, and that's along-side Macsyma and Sage.