在 TPTP 中表示语法上不同的术语
Representing syntactically different terms in TPTP
我正在看一阶逻辑定理证明器，例如 Vampire 和 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 Report 明确指出，不同的双引号字符串确实是不同的对象，所以另一种解决方案是在这里和那里加上引号，从而得到以下无法满足的程序。
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))).
首先让我向您指出 TPTP 的 Syntax BNF。原则上，您有 Prolog 术语和一些具有适当优先级的预定义 infix/prefix 运算符。这意味着，变量以大写字母书写，常量以小写字母书写。也像 Prolog，用单引号转义允许我们写一个以大写字母开头的常量，即 'X'。到目前为止，我从未见过双引号原子，因此您可能需要查看证明者的说明以了解如何解释它们。
但即使语法是 Prolog-ish，自动定理证明也是一种不同的野兽。没有封闭世界的假设，也没有假设不同的常数是不同的——这就是为什么你找不到以下证据的原因：
fof(c1, conjecture, a=b ).
而且都不是：
fof(c1, conjecture, ~(a=b) ).
所以如果你想要句法不等式，你需要公理化它。现在，假设 a 与 b 的不同表明它们是不同的，所以我至少声称："Suppose there are two different constants a and b, then there exists some variable which is not b."
fof(a1, axiom, ~(a=b)).
fof(c1, conjecture, ?[X]: ~(X=b)).
由于一阶逻辑中的函数不一定是单射的，因此您也不必在其中添加假设。
另请注意输入公式的不同作用：到目前为止，您只陈述了公理，没有提出猜想，即您要求证明者证明您的公理集不一致。一些证明者甚至可能会放弃，因为他们使用了一些分辨率改进（例如支持集）来限制公理之间的分辨率[1]。在任何情况下，你都需要知道你试图证明的公式是 A1 ∧ ... ∧ An → C1 ∨ ... Cm 的形式，其中 A 是公理，C 是猜想。[2]
我希望至少语法现在更清晰了 - 不幸的是，问题的答案更多是原子定理证明者没有做出与你期望的相同的假设，所以你必须公理化它们。这些公理化通常也是无效的，您可能会通过专门的工具获得更好的性能。
[1] 正如您已经注意到的，Vampire 或 E Prover 等高级证明器会告诉您有关（反）可满足性的信息。
[2] 基于分辨率的定理证明器将首先否定该公式并执行 CNF 转换，但即使大多数接受 TPTP 的证明器都是基于分辨率的，但这不是必需的。
我正在看一阶逻辑定理证明器，例如 Vampire 和 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 Report 明确指出，不同的双引号字符串确实是不同的对象，所以另一种解决方案是在这里和那里加上引号，从而得到以下无法满足的程序。
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))).
首先让我向您指出 TPTP 的 Syntax BNF。原则上，您有 Prolog 术语和一些具有适当优先级的预定义 infix/prefix 运算符。这意味着，变量以大写字母书写，常量以小写字母书写。也像 Prolog，用单引号转义允许我们写一个以大写字母开头的常量，即 'X'。到目前为止，我从未见过双引号原子，因此您可能需要查看证明者的说明以了解如何解释它们。
但即使语法是 Prolog-ish，自动定理证明也是一种不同的野兽。没有封闭世界的假设，也没有假设不同的常数是不同的——这就是为什么你找不到以下证据的原因：
fof(c1, conjecture, a=b ).
而且都不是：
fof(c1, conjecture, ~(a=b) ).
所以如果你想要句法不等式，你需要公理化它。现在，假设 a 与 b 的不同表明它们是不同的，所以我至少声称："Suppose there are two different constants a and b, then there exists some variable which is not b."
fof(a1, axiom, ~(a=b)).
fof(c1, conjecture, ?[X]: ~(X=b)).
由于一阶逻辑中的函数不一定是单射的，因此您也不必在其中添加假设。
另请注意输入公式的不同作用：到目前为止，您只陈述了公理，没有提出猜想，即您要求证明者证明您的公理集不一致。一些证明者甚至可能会放弃，因为他们使用了一些分辨率改进（例如支持集）来限制公理之间的分辨率[1]。在任何情况下，你都需要知道你试图证明的公式是 A1 ∧ ... ∧ An → C1 ∨ ... Cm 的形式，其中 A 是公理，C 是猜想。[2]
我希望至少语法现在更清晰了 - 不幸的是，问题的答案更多是原子定理证明者没有做出与你期望的相同的假设，所以你必须公理化它们。这些公理化通常也是无效的，您可能会通过专门的工具获得更好的性能。
[1] 正如您已经注意到的，Vampire 或 E Prover 等高级证明器会告诉您有关（反）可满足性的信息。
[2] 基于分辨率的定理证明器将首先否定该公式并执行 CNF 转换，但即使大多数接受 TPTP 的证明器都是基于分辨率的，但这不是必需的。