一阶逻辑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∀a0,1,2：（（P（ x，y，a）∧P（y，z，b））→G（x，z））

但是请注意，这两个是不等于：从理论上讲（可能不在这里） parent/3打电话，可能有ide效果，进一步的基础术语等等。只有Prolog的一个子集映射到这样的逻辑结构。