如何消除条件 Clingo 规则中的不安全性？

Question

我想在 Clingo 中的一组给定起始节点中的所有节点可到达的有向图中定义一组节点。据我了解，这可以通过规则主体中的 conditions 来完成：在规则

中

p(X) :- q(X) : r(X).

在 p/1 的正文中动态生成规则 q(a) 的合取，用于基于事实 a，规则 r(a) 也适用。现在由于某种原因，以下规则集导致在最后一行发现“不安全”变量 X：

% Test case

arc(1,4). arc(2,4). arc(3,5). arc(4,1). arc(4,2). arc(4,3).
start(1). start(4). start(5).

% Define a path inductively, with the base case being path of length 1:

path(A, B) :- arc(A, B).
path(A, B) :- arc(A, X), arc(X, B).
path(A, B) :- arc(A, X), path(X, Y), arc(Y, B).

% A node X is simply reachable/1, if there is a possibly empty path to it
% from a start node or reachable/2 from A, if there is a path to it from A:

reachable(X) :- start(X).
reachable(X) :- start(A), path(A, X).
reachable(X, A) :- path(A, X).

% Predicate all_reach defined by the reachable relation:

all_reach(X) :- reachable(X, A) : start(A).

我想问一下，“不安全”变量是什么意思，我该如何修正这种情况？一个消息来源声称 不安全变量是一个变量，它出现在规则的头部而不是主体 ，这是有道理的，因为符号 :- 表示反向含义.但是，这里似乎不是这样，所以我很困惑。

会不会是start(a)所依据的事实a不成立，所以蕴涵或规则的主体变成空的，导致不安全。是吗？有避免这种情况的标准方法吗？

Answer 1

问题是 all_reach/1 的正文中没有满足至少 X 的某些基础实例的肯定规则。添加行

% Project nodes from arcs

node(X) :- arc(X,Y).
node(Y) :- arc(X,Y).

并将 all_reach/1 规则重新表述为

all_reach(X) :- reachable(X, A) : start(A); node(X).

问题已解决。想要的连词

∧[i=1 → ∞] reachable(d, s[i])

对于所有起始节点 s[i] 和目标节点 d 然后生成为 allreach/1.

的正文

换句话说，当在规则 r/n 的主体 b/m 中使用条件时， b 中必须仍然有一个谓词 p 无条件地 接地对于规则头部中存在的任何变量。否则我们可能会结束停飞期间有歧义或不断扩大的规则，这是不安全的。

如何消除条件 Clingo 规则中的不安全性？

How to remove unsafety in a conditional Clingo rule?

conditional-statements

clingo