Wolfram 语言™

布尔逻辑中的等式证明

如果一组公理都以等式形式表示，即公式之间的相等性是根据理论运算符构建的，则函数 FindEquationalProof 可以根据这些公理形成一个定理的证明。

用 AxiomaticTheory 获取理论的公理集合，如布尔逻辑。可以指定所涉及的运算符和常量的名称。用形式符号（如 a, b, c）表示约束变量。

构建等式的证明。

用图显示从公理（绿色方块）之前的引理到结论（红色方块）的证明流程。三角形和圆形代表不同类型的引理。

或者显示证明步骤的所有详细信息。