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算术（即对自然数和整数的线性算术，加上一些预处理）的决策程序，这就是为什么您的语句real也可以得到证明的原因（因为它归结为整数问题）。它可以处理量词。它所基于的算法称为库珀算法。
• linarith执行Fourier-Motzkin消除来确定实数上的线性算术问题。它也可以证明自然数和整数上的这些属性，但前提是它们也必须包含所有实数。它不能处理量词。
• arith可以概括为的组合presburger和linarith。

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

• algebra 据我所知，适用于代数运算的某些规则（例如可交换性，关联性，逆元素等）来解决目标，这些目标可以通过重新排列诸如群和环的代数结构中的术语来证明
• approximate 使用区间算术计算机柜的具体条件
• sos可以证明多元多项式不等式，例如(x :: real) ? 2 ? y ? 2 ? x + y ? x * y使用平方和证书
• sturm由我编写的，可以计算给定间隔中的实根数，并证明某些单变量实多项式不等式。
• regexp可以证明有关关系的陈述，例如(r ? s?)* = (r ? s)*使用正则表达式。