cur*_*leo 5 solver theorem-proving isabelle
在 Isabelle，我经常发现我可以使用不同的求解器成功地证明一个目标。
通常，我更愿意使用可以证明目标的最弱求解器。根据我目前与 Isabelle 的经验，我目前的理解是，按照强度增加和速度降低的顺序，常见的逻辑求解器排名如下（即何时rule和simp两者都起作用，rule应该使用等）：
rule < simp < auto < fastforce < force
这样对吗？这里blast适合放哪里？
我检查编程和伊莎贝尔/ HOL（PDF）证明和与伊莎贝尔/ HOL具体语义，但无法找到答案。
证明方法的强度通常没有线性排序，并且您的“最弱”一词假设存在一个。尽管如此，我们可以说“auto”通常至少具有“simp”或“rule”的力量，但由于它更强大，它也可以做一些无用的工作，从而导致失败。fastforce、bestsimp 和 Slowsimp 具有相同的能力，但具有不同的证明搜索策略。
我真的不能透露更多细节，但也许其他人可以。