在 Isabelle，我经常发现我可以使用不同的求解器成功地证明一个目标。
通常，我更愿意使用可以证明目标的最弱求解器。根据我目前与 Isabelle 的经验，我目前的理解是，按照强度增加和速度降低的顺序，常见的逻辑求解器排名如下（即何时rule和simp两者都起作用，rule应该使用等）：
rule < simp < auto < fastforce < force
这样对吗？这里blast适合放哪里？
我检查编程和伊莎贝尔/ HOL（PDF）证明和与伊莎贝尔/ HOL具体语义，但无法找到答案。
到目前为止，我在伊莎贝尔（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 -- ?
我需要一个更多的引理来证明这inj? x ? inj? y是荒谬的,作为关于?Agda中不相交联合类型()的更大定理的一部分.
这个结果将直接来自两个构造函数?,即inj?和inj?不相交.那是阿格达的情况吗？我该如何证明？
这是完整的引理:
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Sum
lemma : ? {a b} {A : Set a} {B : Set b} {x : A} {y : B} ? ¬ inj? x ? inj? y
lemma eq = ?