2

我正在查看一阶逻辑定理证明器，例如 Vampire 和 E-Prover，TPTP 语法似乎是要走的路。我更熟悉诸如答案集编程和 Prolog 之类的逻辑编程语法，虽然我尝试参考TPTP 语法的详细描述，但我似乎仍然没有掌握如何正确区分解释和非解释函子（我可能使用错误的术语）。

本质上，我试图通过证明没有模型作为反例来证明一个定理。我的第一个困难是我没想到下面的逻辑程序是可以满足的。

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).

技术报告澄清了不同的双引号字符串确实是不同的对象，所以另一种解决方案是在这里和那里加上引号，从而得到以下无法满足的程序。

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")这不是一个术语，而是f应用于对象的函数"foo"。所以它可能与 function 重合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))).
4

1 回答 1

3

首先让我指出 TPTP 的语法 BNF。原则上，您有一些带有适当优先级的预定义中缀/前缀运算符的 Prolog 术语。这意味着，变量以大写字母书写，常量以小写字母书写。也像 Prolog 一样，使用单引号转义允许我们编写以大写字母开头的常量，即“X”。到目前为止，我从未见过双引号原子，因此您可能需要查看证明者关于如何解释它们的说明。

但即使语法是 Prolog-ish，自动定理证明是另一种野兽。没有封闭世界假设，也没有假设不同的常数不同 - 这就是为什么您找不到以下证明的原因：

fof(c1, conjecture, a=b ).

也不为：

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

所以如果你想有句法不等式，你需要公理化它。现在，假设 a 与 b 不同就表明它们是不同的，所以我至少声称：“假设有两个不同的常数 a 和 b，那么存在一些不是 b 的变量。”

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

由于一阶逻辑中的函数不一定是单射的，因此您也无法在其中添加假设。

还请注意输入公式的不同作用：到目前为止，您只陈述了公理而没有猜想，即您要求证明者证明您的公理集是不一致的。一些证明者甚至可能放弃，因为他们使用了一些限制公理之间分辨率的分辨率改进（例如支持集）[1]。在任何情况下，您都需要注意，您要证明的公式是A1 ∧ ... ∧ An → C1 ∨ ... CmA 是公理而 C 是猜想的形式。 [2]

我希望现在至少语法更清晰一些 - 不幸的是，问题的答案更多的是原子定理证明器没有做出与您期望的相同的假设，因此您必须将它们公理化。这些公理化通常也是无效的，您可能会从专门的工具中获得更好的性能。

[1] 正如您已经注意到的，Vampire 或 E Prover 等高级证明者会告诉您（反）可满足性。

[2] 基于分辨率的定理证明器将首先否定该公式并执行 CNF 转换，但即使大多数接受 TPTP 的证明器都是基于分辨率的，但这不是必需的。

于 2017-06-06T10:11:53.327 回答