到目前为止，我在伊莎贝尔（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 -- ?