邏輯中的有限失效派生

Question

什麼是有限失效派生？駁斥是否與數學意義上的矛盾相同？一般邏輯程序和確定的邏輯程序有什麼區別？

Answer 1

沒有有限失敗的派生。只有失敗的派生樹和有限失敗的派生樹。失敗的派生是以失敗告終的派生。例如：

p :- q. 
p :- p. 
q :- fail. 

由p的第一個規則和q的唯一規則組成的派生是失敗的派生。派生可能不僅失敗，因爲一個未定義的謂詞，如失敗，但也因爲一些頭統一不完全成功。

現在什麼是有限失敗的派生樹。那麼如果你看所有的派生你得到一棵樹。在有限失效的派生樹中，樹是有限的，並且每個派生都是失敗的。有限未能推導樹具有以下良好特性：

- The interpreter terminates. 
- The interpreter does not produce any answer substitution. 

在實際的Prolog系統中，這意味着，冒充你的問題後，你會得到一個雖然沒有經過（在一些Prolog的系統錯誤的顯示）。有趣的是，上述程序不會因查詢p而終止。它是一個無限推導樹的實例，每個推導都失敗了。導出如下：

p - q - fail 
p - p - q - fail 
p - p - p - q - fail 
Etc.. 

有限失敗派生樹的概念是爲定義的Prolog程序定義的。現在可以將Prolog程序的概念擴展爲普通的Prolog程序。在普通的Prolog程序中，主體可能包含負文字。這個想法是，解釋者退步檢查這些文字的有限失敗派生樹。

一個重要的問題是有限失效的推導樹如何與數學推導相關。在目標失敗的情況下，數學語義應該是什麼？我們如何建立一個實現這種語義的解釋器？一類特殊的語義是基於駁斥方法的。這裏我們解釋一個推導爲建立一個矛盾：

P, ~G |= f => P |- G 

這或多或少意味着雙重否定消除和經典邏輯。但是其他邏輯也是有用的。作爲一個開始，你可能要查找下面的書籍：

邏輯應用程序
安爾·內羅德，理查德·肖
第二。版，1997年，施普林格

再見