-
题名几个定理证明方法的商榷
- 1
-
-
作者
梅春亮
胡亚红
-
机构
丽水学院数理学院
-
出处
《丽水学院学报》
2005年第5期84-86,共3页
-
文摘
《数学分析》是数学专业的一门很重要的基础课,作为教材必须内容准确,文字表达简捷易懂。对《数学分析》教材中的几个定理的证明方法进行了探讨,提出了一些看法。
-
关键词
数学分析
定理证明方法
商榷
-
Keywords
mathematical analysis
theorems proof methods
discussion
-
分类号
O174.13
[理学—基础数学]
-
-
题名基于高阶逻辑的定理证明方法及其对策的应用
- 2
-
-
作者
康漫
张杰
李晓娟
关永
-
机构
北京化工大学信息科学与技术学院
首都师范大学信息工程学院
-
出处
《计算机应用与软件》
2017年第11期6-12,共7页
-
基金
国家自然科学基金项目(61572331
61373034)
-
文摘
定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。
-
关键词
定理证明方法
形式化验证
定理证明器
证明方法
对策
-
Keywords
Theorem proving method Formal verification Theorem proving system Proof method Strategy
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
-
题名用五种方法证明柯西中值定理
被引量:9
- 3
-
-
作者
黄德丽
-
机构
湖州师范学院理学院
-
出处
《湖州师范学院学报》
2003年第z1期27-31,共5页
-
文摘
从多角度全方面介绍了微分中值定理中柯西中值定理的五种证明方法,其中有利用构造辅助函数,根据罗尔定理证明;利用闭区间套定理证明;借助引理,并应用反证法证明;用达布(Darboux)定理和反证法证明;利用坐标旋转变换证明等方法,使柯西中值定理更好的被认识、学习。
-
关键词
柯西中值定理
证明
方法
-
分类号
O172.1
[理学—基础数学]
-
-
题名重写对策在基于HOL的形式化证明中的应用
被引量:1
- 4
-
-
作者
张杰
毛丹雯
关永
施智平
-
机构
北京化工大学信息科学与技术学院
首都师范大学信息工程学院
-
出处
《计算机工程与设计》
CSCD
北大核心
2013年第10期3664-3668,共5页
-
基金
国际科技合作与交流基金项目(2011DFG13000)
-
文摘
讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用。通过REWRITE_TAC对策、ASM_REWRITE_TAC对策和RW_TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较。进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题。
-
关键词
定理证明方法
高阶逻辑定理证明系统
形式化证明
目标制导法
重写对策
-
Keywords
theorem proving method
high order logic theorem proving system
formal proving
goal oriented proving method
rewriting tactic
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
-
题名微分中值定理的证明及推广
被引量:1
- 5
-
-
作者
鲁凤菊
-
机构
洛阳师院数学系
-
出处
《洛阳师范学院学报》
2001年第2期14-16,共3页
-
文摘
本文给出了证明微分中值定理时构造辅助函数的两种方法以及微分中值定理在一元函数、多元向量值函数及抽象函数方面的推广 .
-
关键词
本文给出了证明微分中值定理时构造辅助函数的两种方法以及微分中值定理在一元函数、多元向量值函数及抽象函数方面的推广.
-
Keywords
value theorem in different
assistant function
vector function
abstract function
-
分类号
O172
[理学—基础数学]
-