检查一个不平等系统是否需要另一个平等系统？

Question

我有一个不等式系统，但问题是系统中的所有项都是未分配的变量（编辑：所有变量都代表自然数）。就像我想给系统规则一样：

    a + b >= f + h
    f + b >= d + e
    d + b >= a + c

然后询问系统是否有类似的查询

    d + e >= f + g

必须是真的。有谁知道如何在 matlab 或 python 甚至 prolog 中做到这一点？

Answer 1

正如您所澄清的，您正在推理自然数。

您展示的特殊情况是 Presburger 算术 的示例，它是算术的可判定片段。有几个可用的 Presburger 算术 定理证明器，用 Prolog 和其他语言编写。

使用这样的证明者，例如，您可以证明第四个等式不由前三个等式所蕴涵：

?- 有效（a + b >= f + h /\ f + b >= d + e /\ d + b >= a + c ==> d + e >= f + g)。 错误。

这是一个明确的反例：

?- 解（a + b >= f + h /\ f + b >= d + e /\ d + b >= a + c /\ 不是(d + e >= f + g))。 a=0。 b=0。 f=0。 h=0。 d=0。 e=0。 c=0。 g=1。

---

另外，使用 Prolog，您可以使用约束逻辑编程来搜索 整数 或 有理数，分别缩写为 clpfd 和 clpq反例。

例如，在您展示的情况下，并使用 CLP(Q)：

?- { A + B >= F + H, F + B >= D + E， D + B >= A + C， D + E {_1692>0, ...}。

这个答案表明（因为 CLP(Q) 是完整）在 Q 上存在反例，但没有告诉我们公式是否在 整数或自然数。但是，如果这个查询失败了，那么我们就会知道在 Q 上不存在反例因此在 N 上也不存在，这意味着最后一个不等式确实会在 N 上存在.

要使用约束逻辑编程搜索 N 甚至 整数 上的反例，您可以使用 CLP(FD)。例如，您可以发布反例必须满足的约束：

?- A + B #>= F + H #/\ F + B #>= D + E #/\ D + B #>= A + C #/\ #\ (D + E #>= F + G),

您可以通过标签搜索具体的解决方案。但是，这要求所有域都是有限。例如，我们可以从 0..2 开始，然后尝试越来越大的域。这个策略是完整的：如果有一个反例，我们会以这种方式找到它。另一方面，如果不存在反例，请考虑到我们无法从我们还没有找到反例这一事实得出任何关于公式有效性的结论。

在这种情况下，我们很幸运，很快就找到了几个反例：

?- A + B #>= F + H #/\ F + B #>= D + E #/\ D + B #>= A + C #/\ #\ (D + E #>= F + G), Vs = [A,B,C,D,E,F,G,H], 与 ins 0..2 相比， 标签（Vs）。 A = B, B = F, F = H, H = D, D = E, E = C, C = 0, G = 1, Vs = [0, 0, 0, 0, 0, 0, 1, 0] ; A = B, B = F, F = H, H = D, D = E, E = C, C = 0, G = 2, Vs = [0, 0, 0, 0, 0, 0, 2, 0] ; A = F, F = H, H = D, D = E, E = C, C = 0, B = G，G = 1， Vs = [0, 1, 0, 0, 0, 0, 1, 0] ; A = F, F = D, D = E, E = C, C = 0, B = H，H = G，G = 1， Vs = [0, 1, 0, 0, 0, 0, 1, 1] ; A = F, F = H, H = D, D = E, E = C, C = 0, B = 1， G = 2, Vs = [0, 1, 0, 0, 0, 0, 2, 0] 。

总而言之，我建议以下组合：

• 定理证明器优于 Presburger 算术
• CLP(FD)
• CLP(Q)
• 可能还有其他方法

找到此类蕴涵的反例或证明。

请注意，这通常会很快不可判定，但它可以通过线性公式判定。