FindEquationalProof

FindEquationalProof[thm,axms]

尝试使用公理 axms 找到符号定理 thm 的等式证明.

FindEquationalProof[thm,"theory"]

尝试使用指定的命名的公理理论找到 thm 的证明.

更多信息和选项

  • 如果 FindEquationalProof[thm,axms] 成功地从公理 axms 推导出定理 thm，则返回 ProofObject 表达式. 如果成功地证明了该定理不能从公理中得出，它将返回一个 Failure 对象. 否则，除非时间限制，它可能不会终止.
  • 公理和定理可以以等式形式或一阶逻辑中的公式形式给出. 将一阶逻辑中的公式转换为等式.
  • 陈述 thm 和 axms 可以是以下形式的项的逻辑组合：
  • expr1expr2相等性断言
    p[expr1,…]任意符号谓词
    ForAll[vars,stmt]认定对于 vars 的所有值 stmt 为真的断言
    Exists[vars,stmt]认定 stmt 为真时 vars 的值存在的断言
  • expri 可以是任意符号表达式，具有表示正式运算符、函数等的标头.
  • 陈述 stmt 可以包含谓词的任意逻辑组合.
  • FindEquationalProof[expr1&&expr2&&…,axm1&&axm2&&…] 将会把每个 expr1,expr2,… 看作独立的假设，把每个 axm1,axm2,… 看作独立的公理.
  • FindEquationalProof[{expr1,expr2,…},{axm1,axm2,…}] 等价于 FindEquationalProof[expr1&&expr2&&…,axm1&&axm2&&…].
  • FindEquationalProof[thm,"theory"] 等价于 FindEquationalProof[thm,AxiomaticTheory["theory"]].
  • FindEquationalProof["name","theory"] 试图从 AxiomaticTheory["theory","NotableTheorems"] 中求出已命名定理的证明.
  • FindEquationalProof 有下列选项：
  • TimeConstraint Infinity允许使用多长时间
  • 如果 FindEquationalProof 超过了指定的时间限制，将会返回 Failure 对象.
  • FindEquationalProof[thm,axms] 用 Knuth–Bendix 补全算法来证明定理 thm 遵循公理 axms.

范例

打开所有单元关闭所有单元

基本范例  (3)

用命题逻辑证明一个基本定理：

显示抽象证明网络：

用 Dataset 对象显示完整的证明步骤：

用一阶逻辑证明涉及通用附量 (universal quantification) 的定理：

输入自然语言参数：

证明一个简单的三段论：

范围  (3)

根据公理列表证明基本定理：

用连等表示定理：

证明一个等式命题不能从另一个命题中推导出来：

使用存在量词证明谓词逻辑中的三段论：

选项  (1)

TimeConstraint  (1)

用 TimeConstraintt 将计算时间限制在 t 秒内：

默认情况下，FindEquationalProof 会无限期地寻找证明：

应用  (19)

基本逻辑  (6)

为布尔逻辑指定公理选择：

证明贝尔逻辑中的公理：

显示抽象的证明网络：

证明布尔逻辑中的其他公理：

构建和运行相关的证明函数：

指定 Sheffer 逻辑公理：

证明 Sheffer 逻辑中的公理：

显示证明数据集：

证明 Sheffer 逻辑中的其他公理：

构建（并运行）相关的证明函数：

证明 Sheffer 逻辑中的第三公理：

显示抽象证明网络：

证明 Sheffer 逻辑中的最后公理：

显示抽象证明网络：

定义布尔逻辑、Huntington 逻辑和 Robbins 逻辑的公理：

证明亨廷顿逻辑的公理遵循布尔逻辑的公理：

证明罗宾斯逻辑的公理遵循布尔逻辑的公理：

证明罗宾斯逻辑的公理遵循亨廷顿逻辑的公理：

为布尔代数定义 Wolfram 的最短可能公理:

证明 Nand 的交换性：

通过辅助定义引入 And、Or、Not 运算符，用 Wolfram 公理来证明布尔公理：

通过辅助定义引入 Or、Not 运算符，用 Wolfram 公理证明 Or-Not 布尔公理：

抽象代数  (8)

指定群论公理：

证明左边的恒等式存在：

输入自然语言参数：

证明更复杂的群论定理：

显示抽象证明网络：

指定阿贝尔群论的公理：

证明阿贝尔群论的公理：

显示证明数据集：

证明阿贝尔群论中的其他公理：

显示抽象证明网络：

定义半群理论，幺半群理论和群论的公理：

证明每个群都是半群：

证明每个群都是幺半群：

定义阿贝尔群理论和环理论的公理：

证明每个环是阿贝尔群：

取群论的公理，以 p 为乘积，e 为单位元：

添加从其八个元素中的两个生成四元群的关系：

证明群中的其他关系：

场论的公理包括乘法右逆的存在性：

因为乘积是可交换的，所以它们也是左逆的：

通过指定乘积是可交换的，根据左近环的公理证明右近环的公理：

构建幂等半环公理，其中用 LeftTriangle 表示自然定义的偏序：

证明偏序是非对称的：

算术  (1)

为 Presburger 算术的修改（等式）版本指定一些公理：

证明 Presburger 算法中的双否定定理：

显示抽象证明网络：

证明关于 Presburger 算术中加法运算符的公理：

显示证明数据集：

实分析  (1)

这些公理指定微积分基本定理、乘积规则和微分线性：

根据部分公式证明积分：

排版自然语言参数：

循环理论与通用代数  (1)

这些公理描述了一个循环，其内部自同构群是阿贝尔：

证明此循环的幂零性类小于或等于 3：

显示证明数据集：

逻辑难题  (2)

跟随刘易斯·卡洛尔 (Lewis Carroll)，推断婴儿无法管理鳄鱼：

查看 knight（总是说真话）和 knave（总是说谎）难题的解：

属性和关系  (2)

如果 FindEquationalProof 返回一个特定定理的证明对象 (proof object)，针对该定理，FullSimplify 将会返回 True：

FindEquationalProof 把公理列表和公理的组合看作是等价的：

对于假设同样成立：

可能存在的问题  (1)

默认情况下，FindEquationalProof 不能证明涉及算术运算符的定理：

通过指定乘法的性质性证明结果：

Wolfram Research (2018)，FindEquationalProof，Wolfram 语言函数，https://reference.wolfram.com/language/ref/FindEquationalProof.html （更新于 2020 年）.

文本

Wolfram Research (2018)，FindEquationalProof，Wolfram 语言函数，https://reference.wolfram.com/language/ref/FindEquationalProof.html （更新于 2020 年）.

CMS

Wolfram 语言. 2018. "FindEquationalProof." Wolfram 语言与系统参考资料中心. Wolfram Research. 最新版本 2020. https://reference.wolfram.com/language/ref/FindEquationalProof.html.

APA

Wolfram 语言. (2018). FindEquationalProof. Wolfram 语言与系统参考资料中心. 追溯自 https://reference.wolfram.com/language/ref/FindEquationalProof.html 年

BibTeX

@misc{reference.wolfram_2024_findequationalproof, author="Wolfram Research", title="{FindEquationalProof}", year="2020", howpublished="\url{https://reference.wolfram.com/language/ref/FindEquationalProof.html}", note=[Accessed: 21-November-2024 ]}

BibLaTeX

@online{reference.wolfram_2024_findequationalproof, organization={Wolfram Research}, title={FindEquationalProof}, year={2020}, url={https://reference.wolfram.com/language/ref/FindEquationalProof.html}, note=[Accessed: 21-November-2024 ]}