在TPTP中表示語法上不同的術語

Question

我正在研究諸如吸血鬼和E-Prover這樣的一階邏輯定理證明器，並且TPTP語法似乎是要走的路。我對邏輯編程語法比較熟悉，例如Answer Set Programming和Prolog，雖然我嘗試引用TPTP syntax的詳細描述，但我仍然不明白如何正確區分解釋函數和非解釋函子（而且我可能使用術語錯誤）。

本質上，我試圖通過證明沒有模型作爲反例來證明一個定理。我的第一個困難是我沒有想到下面的邏輯程序是可以滿足的。

fof(all_foo, axiom, ![X] : (pred(X) => (X = foo))). 
fof(exists_bar, axiom, pred(bar)). 

，因爲沒有什麼能阻止bar從等於foo這的確是滿足的。所以第一個解決方案是堅持這兩個術語是不同的，我們獲得以下不可滿足的計劃。

fof(all_foo, axiom, ![X] : pred(X) => (X = foo)). 
fof(exists_bar, axiom, pred(bar)). 
fof(foo_not_bar, axiom, foo != bar). 

的Techinal報告闡明瞭不同的雙引號中的字符串是不同的對象確實是，所以另一種解決方案是在這裏和那裏提出報價，從而獲得以下不可滿足的程序。

fof(all_foo, axiom, ![X] : (pred(X) => (X = "foo"))). 
fof(exists_bar, axiom, pred("bar")). 

我很高興沒有手動指定不等式，因爲這顯然不會擴展到更真實的場景。靠近我的真實情況，我實際上必須處理組成條款，並且不幸的是下面的程序是令人滿意的。

fof(all_foo, axiom, ![X] : (pred(X) => (X = f("foo")))). 
fof(exists_bar, axiom, pred(g("bar"))). 

我猜f("foo")不是一個詞，但應用到對象"foo"功能f。所以它可能會與功能g重合。儘管手動規範f和g從來不會一致，但下面的程序是不可滿足的，我覺得我做錯了。它可能不會擴展到我的真實環境，大量的術語在語法上不同時被解釋爲獨特。

fof(all_foo, axiom, ![X] : (pred(X) => (X = f("foo")))). 
fof(exists_bar, axiom, pred(g("bar"))). 
fof(f_not_g, axiom, ![X, Y] : f(X) != g(Y)). 

我嘗試過扔單引號，但我沒有找到正確的方法來做到這一點。

如何製作句法不同（組合）的術語並測試語法上的相等性？

輔助問題：以下程序是可以滿足的，因爲自動定理證明器將f理解爲函數而不是未解釋函數。

fof(exists_f_g, axiom, (?[I] : ((f(foo) = f(I)) & pred(g(I))))). 
fof(not_g_foo, axiom, ~pred(g(foo))). 

爲了使它不可滿足，我需要手動指定f是內射的。沒有指定我的程序中發生的所有函子的注入性，得到這種行爲的自然方法是什麼？

fof(exists_f_g, axiom, (?[I] : ((f(foo) = f(I)) & pred(g(I))))). 
fof(not_g_foo, axiom, ~pred(g(foo))). 
fof(f_injective, axiom, ![X,Y] : (f(X) = f(Y) => (X = Y))). 

Answer 1

首先讓我指點一下TPTP的Syntax BNF。原則上，您有一些Prolog術語，其中包含一些具有適當優先級的預定義中綴/前綴運算符。這意味着，變量以大寫形式寫入，常量以小寫形式寫入。同Prolog一樣，用單引號轉義允許我們寫一個以大寫字母開頭的常量，即'X'。到目前爲止，我從未見過雙引號原子，因此您可能需要查看證明者如何解釋它們的說明。

但即使語法是Prolog-ish，自動定理證明是一種不同的野獸。沒有封閉世界的假設也被認爲是不同的不同的常數 - 這就是爲什麼你不能找到一個證明：

fof(c1, conjecture, a=b). 

既不爲：

fof(c1, conjecture, ~(a=b)). 

所以，如果你想有語法DIS - 平等，你需要公理化它。現在，假設與b不同，他們不同，所以我至少聲稱：「假設有兩個不同的常量a和b，則存在一些不是b的變量。」

fof(a1, axiom, ~(a=b)). 
fof(c1, conjecture, ?[X]: ~(X=b)). 

因爲一階邏輯中的函數不一定是內射的，所以你也不會在那裏添加你的假設。

請注意輸入公式的不同角色：到目前爲止，您只說明瞭公理，並且沒有猜測，即您要求證明者證明您的公理不一致。一些證明者甚至會放棄，因爲他們使用了一些限制公理之間的分辨率的決議細化（例如一組支持）[1]。無論如何，你需要知道你試圖證明的公式是形式A1 ∧ ... ∧ An → C1 ∨ ... Cm，其中A是公理，C是猜測。[2]

我希望至少現在的語法更清晰一些 - 不幸的是，問題的答案更多的是歸納定理證明者不會像您期望的那樣做出相同的假設，因此您必須對它們進行公理化。這些公理化通常也是無效的，你可能會從專門的工具中獲得更好的性能。正如你已經注意到的那樣，高級證明者如吸血鬼或者E證明者反而告訴你（反） - 滿足性。

[2]基於分辨率的定理證明器將首先否定該公式並執行CNF變換，但即使大多數TPTP接受證明者是基於分辨率的，這不是要求。