一阶逻辑 Prolog 匿名变量

Question

下面的Prolog规则：

grandparent(X,Z) :- parent(X,Y) , parent(Y,Z)

在一阶逻辑中将是：

∀x ∀y ∀z ((P (x, y) ∧ P (y, z)) → G(x, z))

理论上，如果我们在Prolog规则中有一个匿名变量，如下所示：

grandparent(X,Z) :- parent(X,Y, _ ) , parent(Y,Z, _ )

假设它是一个姓氏，我们如何用一阶逻辑来呈现它？

Answer 1

只需使用规则：

"给孩子起个名字">

请注意，下划线不是单个变量。Prolog中的两个下划线彼此无关。

我们可以简单地将代码替换为：

grandparent(X,Z) :-
parent(X,Y,A),
parent(Y,Z,B).

现在一个合乎逻辑的">等价物"将是：

∀x ∀y ∀z ∀a ∀b： ((P (x， y， a( ∧ P (y， z， b((→ G(x， z((

但请注意，这两者并不等同：因为从理论上讲(可能不是在这里(，第一次parent/3调用可能会产生副作用，进一步的基本项等。只有Prolog的子集映射到这样的逻辑结构。