单元传播

单元传播单元传播（UP）或布尔约束传播（BCP）或单字规则（OLR）是一种自动定理证明程序，可以简化一组（通常是命题）条款。单元传播的定义该程序基于单元子...