到目前为止，我在 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 -- ✘
最佳答案
我刚刚问了 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)*。