“最好”的方法取决于您具体的使用情况！这是另一种使用clpfd的方法：
:- use_module(library(clpfd)).
我们根据@mat在对
相关问题的先前答案的评论中提出的建议，定义谓词
equidistant_stride/2 ：
equidistant_stride([],_).
equidistant_stride([Z|Zs],D) :-
foldl(equidistant_stride_(D),Zs,Z,_).
equidistant_stride_(D,Z1,Z0,Z1) :-
Z1 #= Z0+D.
基于equidistant_stride/2，我们定义：
consecutive_ascending_integers(Zs) :-
equidistant_stride(Zs,1).
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
consecutive_ascending_integers_from(Zs,1).
让我们运行一些查询！首先是您的原始用例：
?- length(Zs,N), consecutive_ascending_integers_from_1(Zs).
N = 1, Zs = [1]
; N = 2, Zs = [1,2]
; N = 3, Zs = [1,2,3]
; N = 4, Zs = [1,2,3,4]
; N = 5, Zs = [1,2,3,4,5]
...
使用 clpfd，我们可以提出相当普遍的查询，并获得逻辑上正确的答案！
？- consecutive_ascending_integers([A,B,0,D,E]).
A = -2，B = -1，D = 1，E = 2。
？- consecutive_ascending_integers([A,B,C,D,E]).
A + 1 # = B，B + 1 # = C，C + 1 # = D，D + 1 # = E。
一个替代实现的equidistant_stride/2:
我希望新的代码能更好地利用约束传播。
感谢@WillNess提供的测试用例，激励了这次重写！
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,N,D) :-
Z #= Z0 + N*D,
N1 #= N+1,
equidistant_from_nth_stride(Zs,Z0,N1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
equidistant_from_nth_stride(Zs,Z0,1,D).
使用@mat的clpfd进行旧版与新版的比较：
首先，是旧版：
?- equidistant_stride([1,_,_,_,14],D).
_G1133+D#=14,
_G1145+D#=_G1133,
_G1157+D#=_G1145,
1+D#=_G1157.
?- equidistant_stride([1,_,_,_,14|_],D).
_G1136+D#=14, _G1148+D#=_G1136, _G1160+D#=_G1148, 1+D#=_G1160
; 14+D#=_G1340, _G1354+D#=14, _G1366+D#=_G1354, _G1378+D#=_G1366, 1+D#=_G1378
...
现在让我们切换到新版本并询问相同的查询！
？- equidistant_stride([1，_，_，_，14]，D）。
false。 ％失败，正如应该的那样
？- equidistant_stride([1，_，_，_，14 | _]，D）。
false。 ％失败，正如应该的那样
再来一些！我们是否可以通过暂时使用冗余约束条件更早地失败？
以前，我们建议使用约束条件 Z1 #= Z0+D*1，Z2 #= Z0+D*2，Z3 #= Z0+D*3 代替 Z1 #= Z0+D，Z2 #= Z1+D，Z3 #= Z2+D
（这是本答案中的第一个代码版本）。
再次感谢@WillNess通过指出目标 equidistant_stride([_,4,_,_,14],D)不会失败，而是成功并具有待处理的目标，从而激发了这个小实验：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2650, 4, _G2656, _G2659, 14],
14#=_G2650+4*D,
_G2659#=_G2650+3*D,
_G2656#=_G2650+2*D,
_G2650+D#=4.
让我们使用equidistantRED_stride/2添加一些冗余约束：
equidistantRED_stride([],_).
equidistantRED_stride([Z|Zs],D) :-
equidistant_from_nth_stride(Zs,Z,1,D),
equidistantRED_stride(Zs,D).
示例查询：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
false.
完成了吗？还没有！通常情况下，我们不希望有二次冗余约束条件。原因如下：
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2683, _G2686, _G2689, _G2692, 14],
14#=_G2683+4*D,
_G2692#=_G2683+3*D,
_G2689#=_G2683+2*D,
_G2686#=_G2683+D.
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
Zs = [_G831, _G834, _G837, _G840, 14],
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
D+_G840#=14,
14#=2*D+_G837,
_G840#=D+_G837,
14#=_G834+3*D,
_G840#=_G834+2*D,
_G837#=_G834+D.
但是，如果我们使用双重否定的技巧，即使成功的情况下，残留物仍然存在...
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
Zs = [_G454, _G457, _G460, _G463, 14],
14#=_G454+4*D,
_G463#=_G454+3*D,
_G460#=_G454+2*D,
_G457#=_G454+D.
... and ...
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
错误。
...我们比以前检测到了更多的失败案例！
让我们深入探讨一下！我们能否在更广泛的使用中尽早检测到失败？
到目前为止，使用的代码中这两个逻辑上错误的查询不会终止：
?- Zs = [_,4,_,_,14|_], \+ \+ equidistantRED_stride(Zs,D), equidistant_stride(Zs,D).
... % 执行已终止
?- Zs = [_,4,_,_,14|_], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
... % 执行已终止
有修复方法吗？有黑客技巧！
?- use_module(library(lambda)).
true.
?- Zs = [_,4,_,_,14|_],
\+ ( term_variables(Zs,Vs),
maplist(\X^when(nonvar(X),integer(X)),Vs),
\+ equidistantRED_stride(Zs,D)),
equidistant_stride(Zs,D).
false.
该 hack 不能保证冗余约束“part”的终止，但在我看来，这对于快速第一次尝试来说并不太糟糕。在任何变量实例化为
Zs中的单个变量时，测试
integer/1旨在允许
clpfd求解器将变量域约束为单例，而使用 cons-pairs 进行实例化（直接导致基于列表的谓词的非终止）被抑制。
我确实意识到这种 hack 可以很容易地以多种方式被破解（例如，使用循环术语）。欢迎任何建议和评论！
chain(List, #<)恰好做到了你要求的：它可以用于严格升序整数的列表。使用CLP(FD)约束是描述这样一个列表最优雅和通用的方法。使用numlist/3的解决方案不够通用：它只适用于以特定整数开始，并以1为增量进行排序的具体列表，而不是真正描述“升序整数列表”的通用关系。 - mat