https://zhuanlan.zhihu.com/p/1906322636088256249
第一版相比上一版，从networkx和pulp改用了z3-solver库。原文共三部分，先中文化了前两部分相关运行输出。代码 在此。与上文运行环境相同。
此版代码量约初版的三倍。支持更多功能，结构也更复杂，比如为支持逻辑运算符与、或、否，仅类型定义与简化处理就有一百行左右。另一方面，貌似去掉了有向图。
基于 原库说明 Propositional logic 部分。
例子 more_tactic_examples 输出：
证明目标：假设：(A OR B), (C OR D), 求证：((A AND C) OR (B AND C) OR (A AND D) OR (B AND D))
采用方法——多次简化和分情况：
当前目标：假设：(A OR B), (C OR D), 求证：((A AND C) OR (B AND C) OR (A AND D) OR (B AND D))
简化当前目标中的假设和求证目标……
将假设 (A OR B) 分情况
当前目标：假设：(C OR D), A, 求证：((A AND C) OR (B AND C) OR (A AND D) OR (B AND D))
简化当前目标中的假设和求证目标……
简化 ((A AND C) OR (B AND C) OR (A AND D) OR (B AND D)) 为 (C OR (B AND D) OR D OR (B AND C)).
将假设 (C OR D) 分情况
当前目标：假设：A, C, 求证：(C OR (B AND D) OR D OR (B AND C))
简化当前目标中的假设和求证目标……
简化 (C OR (B AND D) OR D OR (B AND C)) 为 TRUE.
当前目标得证；
当前目标：假设：A, D, 求证：(C OR (B AND D) OR D OR (B AND C))
简化当前目标中的假设和求证目标……
简化 (C OR (B AND D) OR D OR (B AND C)) 为 TRUE.
当前目标得证；
当前目标：假设：(C OR D), B, 求证：((A AND C) OR (B AND C) OR (A AND D) OR (B AND D))
简化当前目标中的假设和求证目标……
简化 ((A AND C) OR (B AND C) OR (A AND D) OR (B AND D)) 为 ((A AND C) OR C OR D OR (A AND D)).
将假设 (C OR D) 分情况
当前目标：假设：B, C, 求证：((A AND C) OR C OR D OR (A AND D))
简化当前目标中的假设和求证目标……
简化 ((A AND C) OR C OR D OR (A AND D)) 为 TRUE.
当前目标得证；
当前目标：假设：B, D, 求证：((A AND C) OR C OR D OR (A AND D))
简化当前目标中的假设和求证目标……
简化 ((A AND C) OR C OR D OR (A AND D)) 为 TRUE.
所有目标得证！
可见其逐步列出了所有四种情况 A&C, A&D, B&C, B&D。思路有点像第0版中的穷举法。
好奇用像 Prolog 会如何处理类似问题。
对应 原库说明 simple multiplicative inequalities 部分
feasbility_examples 输出：
检验以下不等式可否成立：
1*x + 1*y >= 5
1*y <= 2
1*x <= 3
以下取值可成立
y = 2
x = 3
检验以下不等式可否成立：
1*x + 1*y >= 5
1*y <= 2
1*x + 1*y > 5
1*x <= 3
以下式子取和，得证不可能成立：
1*y <= 2 两边乘 -1
1*x + 1*y > 5 两边乘 1
1*x <= 3 两边乘 -1
检验以下不等式可否成立：
2*x + -1*y = 0
1*y > 3
1*x < 2
以下取值可成立
y = 10/3
x = 5/3
举例让不等式组成立是个新奇功能。让我想起 为正则表达式举例的设想。粗看是基于 z3-solver 实现的。
log_linarith_example2 输出：
证明目标：假设：X <~ Y, Z << W, Z ~ U, 求证：(X * (Z ^ 2)) << (Y * U * W)
假设 (X * (Z ^ 2)) << (Y * U * W) 不成立。
用 logarithmic linear arithmetic 反证……
以下之积可得矛盾：
Z * W^-1 << 1 的 -1 次幂
Z * U^-1 ~ 1 的 -1 次幂
X * Z^2 * Y^-1 * U^-1 * W^-1 >~ 1 的 1 次幂
X * Y^-1 <~ 1 的 -1 次幂
所有目标得证！
上面四个不等式之积会得出 1>1，因而矛盾。
log_linarith_example_2 输出：
证明目标：假设：(x ^ 2) << y, (y ^ 2) << z, 求证：x <~ z
假设 x <~ z 不成立。
用 logarithmic linear arithmetic 反证……
很不幸，假设之积可成立。反例（当N够大）：
y = N^-5/6
z = N^-7/6
x = N^-2/3
居然能举出反例，回头要研究这个z3。
例子 expression_examples 输出：
预估为： (((((a + b + c) ^ 1/2) * (a + b) * (max(a, c, b) ^ 1/2)) / (((1 + (d ^ 2)) ^ 1/2) * max(a, b))) ^ 2)
简化后： ((max(a, b, c) ^ 2) * (max(1, (d ^ 2)) ^ -1))
这里用到不少运算符重载，感觉相对用rply等解析方法，会省去不少parser的调试开销，不失为快速搭原型的有效方法。
例子 simp_example 输出：
证明目标：求证：((((x * (y ^ 1/2)) ^ 4) * 3) / x) << (z * y * (z ^ -2))
简化当前目标中的假设和求证目标……
简化 ((((x * (y ^ 1/2)) ^ 4) * 3) / x) << (z * y * (z ^ -2)) 为 ((z ^ -1) * (y ^ -1) * (x ^ -3)) >> 1.
1. [当前目标] 求证：((z ^ -1) * (y ^ -1) * (x ^ -3)) >> 1