伊莎贝尔的 "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)* 等关系的陈述。