一階邏輯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的一個子集映射到這樣的邏輯結構。