Prolog順序的統一

我剛開始嘗試自學Prolog，在七週內同時使用七種語言和現在學習Prolog！我遇到了一些困惑。在SLSW有一天它呈現以下知識庫：Prolog順序的統一

cat(lion). 
cat(tiger). 

dorothy(X,Y,Z):- X = lion, Y = tiger, Z = bear. 
twin_cats(X,Y):- cat(X), cat(Y).

當與twin_cats(X,Y).問，它生產的所有的可能性兩隻貓，包括X = lion, Y = lion和X = tiger, Y = tiger。亂七八糟的是我試圖給twin_cats(X,Y)規則添加一個目標，以便它只報告兩隻不同的貓。起初，我試圖

cat(lion). 
cat(tiger). 

dorothy(X,Y,Z):- X = lion, Y = tiger, Z = bear. 
twin_cats(X,Y):- \+(X = Y), cat(X), cat(Y).

要其序言迴應no到twin_cats(X,Y).然而，當我剛換的目標，爲了

cat(lion). 
cat(tiger). 

dorothy(X,Y,Z):- X = lion, Y = tiger, Z = bear. 
twin_cats(X,Y):- cat(X), cat(Y), \+(X = Y).

序言現在給我什麼，我一直在尋找，兩個答案X = lion, Y = tiger和X = tiger, Y = lion。

所以這是我的問題，Prolog統一變量的方式是否存在一些固有的順序？這似乎是因爲目標的順序（即使它們全部由and分開）都會改變查詢的結果。在第二個工作KB中，我想我知道它是如何統一的。首先統一爲cat(X)，然後cat(Y)然後檢查它們是否相同。如果他們移動到下一個組合等，直到沒有組合，並報告通過所有三個目標的兩個案例。但是對於第一個KB，當它首先檢查是否X = Y時，該目標是否應該是真的，因爲變量尚未統一？

來源

2014-12-06 celeriko

Prolog統一**術語**，其中變量只是一個重要的情況 – CapelliC 2014-12-06 19:00:53

[在Prolog查詢中帶有變量的\\ \\ \\問題]的可能重複（http://stackoverflow.com/questions/5971967 /帶有變量的序列查詢問題） – celeriko 2014-12-06 19:18:06

'\ +（X = Y）'表示「'X'不能與'Y'統一。 - 變量統一是匹配的一部分，這是一種證明目標的機制，它按照從左到右的順序完成，就像它們被寫入一樣。 – 2014-12-06 21:49:32

所以這是我的問題，是否有一些固有的排序方式，Prolog統一變量？

是，序言試圖在你寫的爲了統一（和失敗，如果不能夠）：

clause:- 
    <unifies first>, 
    <unifies second>…

您尤其可以看到，經過trace.（這是SWI），變量名稱由內部名稱改爲：

[trace] ?- twin_cats(X,Y). 

true. 

    Call: (6) twin_cats(_G970, _G971) ? creep 
    Call: (7) cat(_G970) ? creep 
    Exit: (7) cat(lion) ? creep 
    Call: (7) cat(_G971) ? creep 
    Exit: (7) cat(lion) ? creep 
    Call: (7) lion=lion ? creep 
    Exit: (7) lion=lion ? creep 
    Redo: (7) cat(_G971) ? creep 
    Exit: (7) cat(tiger) ? creep 
    Call: (7) lion=tiger ? creep 
    Fail: (7) lion=tiger ? creep 
    Redo: (6) twin_cats(lion, tiger) ? creep 
    Exit: (6) twin_cats(lion, tiger) ? creep 
X = lion, 
Y = tiger ; % first redo 
    Redo: (7) cat(_G970) ? creep 
    Exit: (7) cat(tiger) ? creep 
    Call: (7) cat(_G971) ? creep 
    Exit: (7) cat(lion) ? creep 
    Call: (7) tiger=lion ? creep 
    Fail: (7) tiger=lion ? creep 
    Redo: (6) twin_cats(tiger, lion) ? creep 
    Exit: (6) twin_cats(tiger, lion) ? creep 
X = tiger, 
Y = lion ; % second redo 
    Redo: (7) cat(_G971) ? creep 
    Exit: (7) cat(tiger) ? creep 
    Call: (7) tiger=tiger ? creep 
    Exit: (7) tiger=tiger ? creep 
    Fail: (6) twin_cats(_G970, _G971) ? 
false.

Furhermore，\+不unifiy。它也沒有對變量設置任何限制，以便他們以後可以統一。它只是調用後來發生的事情，如果它真的發生了，就會失敗

來源

2014-12-06 23:21:51

Prolog順序的統一

回答

相關問題