Prolog 子句的溯因

Question

我有一个带有标记节点和边的有向根图的规范。该规范描述了哪些节点可以连接到哪些其他节点，以及根据顶点属性的图结构的各个方面。

例如：

每个 A 节点都必须连接到具有边类型 B 的 B 节点，该 B 节点通过任何边类型连接到 D 节点，并且根必须具有到至少 2 个其他节点的路径。

followsSpec(Root) :- 
    edge(Root, _, A), 
    edge(Root, _, B), 
    A != B, 
    edge(A, edgeTypeB, C), 
    node(C, nodeTypeC), 
    edge(C, _, D),
    node(D, nodeTypeD).

我想说

node(root, typeA)
followsSpec(root)

并引出图表中使followsSpec 为真的其他可能元素：

node(b, typeB)
node(c, typeC)
edge(root, some_arbitrary_edge_type, b)
edge(root, some_other_arbitrary_edge_type, c)
edge(b, edge_type_b, c)

有没有办法在 Prolog 中做到这一点？

我特别担心效率，因为实际上规范更复杂，至少会有 100 个节点。

编辑：试图形式化： 可溯源谓词是edge/3（其中三个变量对应于转换的源、目标和类型）和node/2（其中两个变量对应于节点标识符和节点标签）。
我从一个事实开始node(root, rootLabel))。 我的观察：followsSpec(root)，其中

followsSpec(X) :- "x is connected in a particular way to other nodes through edges"

我想观察的：那些其他节点和边是什么，所以 followSpec(root) 是真的。

Answer 1

您可以使用假设推理来找到溯因解决方案。假设您有一个理论 T，并且想为某些观察 O 找到解释 E：

 T, E |- O

假设推理有一个特殊的运算符，称为嵌入蕴涵 (assumez)。您可以使用这个蕴涵来验证溯因解，将溯因转化为演绎：

 T |- assumez(E, O).

假设z/2 的简单实现是：

assumez(E,O) :-
   assertz(E),
   O,
   retract(E).

但上述内容将无法幸免，因此您需要一个已跟踪 assertz/1 和retract/1 的 Prolog 系统。如果您不想使用 CHR 或 ASP，可以使用 Jekejeke Prolog 中更简单的库（最小/低）。