检查逻辑表达式/规格说明等价性的高效算法是什么？

当然有，针对不同复杂度的表达式，常用的高效方法主要有以下几种：

• 范式标准化对比
  把任意布尔表达式转化为合取范式（CNF）或析取范式（DNF），然后对范式做标准化处理（比如排序子句、移除重复项、合并等价子句），最后直接对比标准化后的范式是否完全一致。比如你举的两个例子，转化为CNF后都是(age >= 13) ∧ (gender == Gender.Female)，标准化后结构完全相同，就能判定等价。
  这种方法简单直接，但缺点是复杂表达式的范式可能出现指数级膨胀，只适合中小规模的场景。

• SAT/SMT求解器验证
  逻辑等价的核心是：表达式A和B等价，当且仅当A ↔ B是永真式，也就是(A ∧ ¬B) ∨ (¬A ∧ B)是永假式。把这个待验证的式子交给现代SAT求解器（基于CDCL算法），如果求解器返回不可满足（UNSAT），就说明A和B逻辑等价。
  如果你的表达式包含数值比较、枚举类型这类非纯布尔逻辑的约束，可以用SMT求解器（比如Z3、CVC4）扩展，它能处理布尔逻辑+算术理论+枚举理论的组合场景。现代SAT/SMT求解器能高效处理大规模、层级复杂的表达式，是工业界常用的方案。

• 表达式树结构规范化
  对表达式树做递归的规范化变换：比如利用交换律统一二元操作数的顺序（把A ∧ B和B ∧ A调整为相同的结构）、消除冗余节点（比如A ∧ A简化为A）、用德摩根定律统一否定运算符的位置、递归标准化所有子节点。
  规范化完成后，直接对比两棵表达式树的结构是否完全一致即可。这种方法效率极高，但只能处理可以通过简单语法变换覆盖的等价情况，对于需要复杂逻辑推导的等价性（比如A ∧ (B ∨ C)和(A ∧ B) ∨ (A ∧ C)），需要先应用分配律做变换，否则无法识别。

总结下来：如果是小规模纯布尔表达式，范式或结构规范化足够；如果是大规模或带复杂约束的表达式，SAT/SMT求解器是更可靠高效的选择。

内容的提问来源于stack exchange，提问作者Pavel Voronin