The testing for types needs to distinguish itself from the traditional “type testing” built-ins that implicitly also test for a sufficient instantiation. So we effectively test only for sufficiently instantiated terms (si). And if they are not sufficiently instantiated, an appropriate error is issued. For a type nn, there is thus a type testing predicate … Read more
This site is devoted to solve such puzzles with CLP(FD). But the full power of CLP(FD) is overkill here: your assignment can be solved effectively searching the entire solution space when you have adequately described the constraints. The solution will be composed of 5 houses, where each attribute satisfy all constraints imposed by description. Be … Read more
What’s probably more useful than a slightly less nondeterministic length/2 is a proper list-length constraint. You can find an ECLiPSe implementation of it here, called len/2. With this you get the following behaviour: ?- N :: 1..3, len(Xs, N). N = N{1 .. 3} Xs = [_431|_482] % note it must contain at least one … Read more
As a general remark you will find more on SO about it under the name library(pio). Also the way to use it cleanly is rather: :- use_module(library(pio)). Your example is way too complex, so I will only consider a slightly simpler case, a newline separated list of numbers: nats([]) –> []. nats([N|Ns]) –> nat(N), newline, … Read more
In place of not(X = Y) you need to write \+ X = Y or X \= Y. But consider to use dif(X,Y) instead. dif/2 is present in B, SWI, YAP, SICStus. To see the difference: ?- X = b, dif(a, X). X = b. ?- X = b, \+ a = X. X = … Read more
The actual reason for your problem is (\==)/2 within different/2. It succeeds simply too often. Replace it with dif/2 and you will get the expected behavior. dif/2 is available in many Prolog systems like SICStus, YAP, B, SWI. You can also define a safe approximation in ISO-Prolog like so: iso_dif(X, Y) :- X \== Y, … Read more
You have been using cut and an unsafe form of negation. Both have to be used with extreme care. An immediate fix would be to guard your program against uses it is not designed for: unique(X, Xs) :- iwhen(ground(X+Xs), your_unique(X, Xs)). This uses iwhen/2 which is similar to when/2 except that it does not delay: … Read more
If you want to study termination properties in depth, programs using successor-arithmetics are an ideal study object: You know a priori what they should describe, so you can concentrate on the more technical details. You will need to understand several notions. Universal termination The easiest way to explain it, is to consider Goal, false. This … Read more
Well for one thing, the name should be more declarative, like equality_truth/2.
The following is based on the reification of term equality/inequality. First, we first define list_memberd_t/3, which behaves just like the memberd_truth/3 but has a different argument order: list_memberd_t([] ,_,false). list_memberd_t([Y|Ys],X,Truth) :- if_(X=Y, Truth=true, list_memberd_t(Ys,X,Truth)). list_memberd_truth(Xs,X,Truth) :- list_memberd_t(Xs,X,Truth). For the sake of brevity, let’s define memberd_t/3 based on list_memberd_t/3: memberd_t(X,Xs,Truth) :- list_memberd_t(Xs,X,Truth). As a parallel to … Read more