https://zhuanlan.zhihu.com/p/1906712430588962744

接上文，对应 原库第三部分 addition and max/min。

max_lt_min_example 输出：

证明目标：求证：min(a, b) <~ max(a, b)
创建新变量："min(a, b)", "max(a, b)"
1. [当前目标] 假设：a >~ "min(a, b)", a <~ "max(a, b)", b <~ "max(a, b)", b >~ "min(a, b)", (a ~ "min(a, b)" OR b ~ "min(a, b)"), (a ~ "max(a, b)" OR b ~ "max(a, b)"), 求证："min(a, b)" <~ "max(a, b)"

假设 "min(a, b)" <~ "max(a, b)" 不成立。
用 logarithmic linear arithmetic 反证……
以下之积可得矛盾：
a * "min(a, b)"^-1 >~ 1 的 1 次幂
a * "max(a, b)"^-1 <~ 1 的 -1 次幂
"min(a, b)" * "max(a, b)"^-1 >> 1 的 1 次幂
所有目标得证！

am_gm_example 输出：

证明目标：求证：((a * b * c) ^ 1/3) <~ ((a + b + c) / 3)
创建新变量："(a + b + c)"
假设 ((a * b * c) ^ 1/3) <~ ("(a + b + c)" / 3) 不成立。
用 logarithmic linear arithmetic 反证……
以下之积可得矛盾：
b * "(a + b + c)"^-1 <~ 1 的 -1/3 次幂
c * "(a + b + c)"^-1 <~ 1 的 -1/3 次幂
a^1/3 * b^1/3 * c^1/3 * "(a + b + c)"^-1 >> 1 的 1 次幂
a * "(a + b + c)"^-1 <~ 1 的 -1/3 次幂
所有目标得证！

这时发现，“以下之积”的几个不等式的排序不确定。

最后来到 autosolve，会尝试之前的所有简化、反证、分情况等方法对目标进行试解。

因为太长，LP_autosolve_example 的 输出在此。第一次运行的输出有三百多行，和原文中比较多了一百行。

多次试验后，发现每次输出从两百多到四百多行不等，怀疑是用于保存目标（ProofState.goals）的数据结构（set）的出入顺序不确定导致的：

class ProofState:
    def __init__(self, goals=()):
        self.goals = set(goals)

但看几百行输出太耗时，尤其是长达三四行的假设列表。遂试了一遍其他例程，看能否用简短输出重现此现象。

幸运发现 more_tactic_examples 的输出有 47行 到 145行。

第十行开始比较：

当前目标：假设：(NOT A OR NOT C), (A OR B), (NOT A OR NOT D), (C OR D), (NOT B OR NOT D), NOT B, 求证：FALSE
简化当前目标中的假设和求证目标……
简化 (NOT B OR NOT D) 为 TRUE.
用 logarithmic linear arithmetic 反证……

当前目标：假设：(NOT A OR NOT D), (NOT B OR NOT C), (C OR D), (NOT B OR NOT D), (NOT A OR NOT C), A, 求证：FALSE
简化当前目标中的假设和求证目标……
简化 (NOT A OR NOT D) 为 NOT D.
简化 (NOT B OR NOT D) 为 TRUE.
简化 (NOT A OR NOT C) 为 NOT C.
简化 (NOT B OR NOT C) 为 TRUE.

可见假设排序不同导致处理路径不同。然后看到目标中的假设也是set：

class Goal:
    def __init__(self, conclusion, hypotheses=()):
        self.conclusion = MutableType(conclusion)
        self.hypotheses = {MutableType(hypothesis) for hypothesis in hypotheses}

不仅初始化时会牵扯顺序，比如反证时会把结论取反后添为假设，也会在set添加元素（顺便将目标变为假）：

    goal.add_hypothesis(conclusion.negate())
    goal.replace_conclusion(Bool(False))

有点感觉像找迷宫的搜索过程，短路和长路可能差很远。下面看看最新版是否也类似。