伊莎贝尔语中的“arith”和“presburger”有什么区别？

到目前为止，我在伊莎贝尔遇到的每一个目标都可以通过使用来解决arith也可以通过以下方式解决presburger反之亦然，例如

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

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

Edit:我设法想出了一个引理，证明了arith that 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 -- ✘

我刚刚问过托拜厄斯·尼普科夫（Tobias Nipkow），他是这么告​​诉我的：

• presburger是一个决策程序普雷斯堡算术 http://en.wikipedia.org/wiki/Presburger_arithmetic，即自然数和整数的线性算术，加上一些预处理，这就是为什么你的陈述real也可以被证明（因为它归结为整数问题）。它可以处理量词。其背后的算法称为库珀算法。
• linarith施行傅里叶-莫茨金消除法 http://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination解决实数线性算术问题。它还可以在自然数和整数上证明这些性质，但前提是它们也适用于所有实数。它无法处理量词。
• arith可以概括为以下组合presburger and linarith.

为了完整起见，我想补充一点，对于有趣的陈述类别有更专门的证明方法：

• algebra使用 Gröbner 基来解决可以通过重新排列代数结构（如群和环）中的项来证明的目标
• approximate使用区间算术计算具体项的包围
• sos可以证明多元多项式不等式(x :: real) ≥ 2 ⟹ y ≥ 2 ⟹ x + y ≤ x * y使用平方和证书
• sturm，这是我写的，可以计算给定区间内的实根数，并证明某些单变量实多项式不等式。
• regexp可以证明有关关系的陈述，例如(r ∪ s⁺)* = (r ∪ s)*使用正则表达式。