solver - Isabelle 中的 "arith"和 "presburger"有什么区别？

Question

到目前为止，我在 Isabelle 遇到的每个目标都可以使用 arith 解决。也可以通过 presburger 解决反之亦然，例如

lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n"
by presburger (* or arith *)

这两个求解器有什么区别？ 一个可以解决但另一个不能解决的目标的例子会很好。

编辑:我设法想出了一个由 arith 证明的引理那个presburger处理不了。这似乎与实数有关:

lemma "max i (i + 1) > (i::nat)" by arith       -- ✔
lemma "max i (i + 1) > (i::nat)" by presburger  -- ✔

lemma "max i (i + 1) > (i::real)" by arith      -- ✔
lemma "max i (i + 1) > (i::real)" by presburger -- ✘

Answer 1

我刚刚问了 Tobias Nipkow，他是这样告诉我的:

presburger是 Presburger arithmetic 的决策程序，即自然数和整数的线性算术，加上一些预处理，这就是为什么你的语句带有 real也可以证明(因为它归结为整数问题)。它可以处理量词。它的底层算法被称为库珀算法。

linarith执行 Fourier-Motzkin elimination决定关于实数的线性算术问题。它还可以证明自然数和整数的这些性质，但前提是它们也适用于所有实数。它无法处理量词。

arith可以概括为presburger的组合和 linarith .

为了完整起见，我想补充一点，对于有趣的语句类有更专门的证明方法:

algebra使用 Gröbner 基解决可以通过重新排列代数结构(如群和环)中的项来证明的目标

approximate使用区间算法计算具体项的包围

sos可以证明多元多项式不等式，如 (x :: real) ≥ 2 ⟹ y ≥ 2 ⟹ x + y ≤ x * y使用平方和证书

sturm ，这是我写的，可以计算给定区间内实根的数量，并证明某些单变量实多项式不等式。

regexp可以证明关于关系的陈述，如 (r ∪ s⁺)* = (r ∪ s)*使用正则表达式。