检索结果-南通市图书馆

布尔代数的广义Fuzzy子代数及其在mizar系统中的实现

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

布尔代数的广义Fuzzy子代数及其在Mizar系统中的实现

作者：孙中品青岛科技大学

学位级别：硕士

本文基于布尔代数的Fuzzy子代数已有的性质，讨论了布尔代数的(∈，∈∨q)-Fuzzy子代数、阈值Fuzzy子代数和Fuzzy子代数的直积的一些性质，进一步丰富和发展了Fuzzy代数系统的基本理论。此外还在mizar系统中实现了关于布尔代数的Fuzzy... 详细信息

本文基于布尔代数的Fuzzy子代数已有的性质，讨论了布尔代数的(∈，∈∨q)-Fuzzy子代数、阈值Fuzzy子代数和Fuzzy子代数的直积的一些性质，进一步丰富和发展了Fuzzy代数系统的基本理论。此外还在mizar系统中实现了关于布尔代数的Fuzzy子代数和(∈，∈∨q)-Fuzzy子代数的mizar定义和相关重要定理的证明，在一定程度上充实了mizar数据库的内容。本文主要取得以下结果：1．利用Fuzzy点与Fuzzy子集的“属于”和“重于”关系，提出了布尔代数的(∈，∈∨q)-Fuzzy子代数、(∈，∈∨q)-Fuzzy理想和(∈，∈∨q)-Fuzzy商布尔代数的概念，给出了布尔代数的Fuzzy子集是(∈，∈∨q)-Fuzzy子代数的充要条件，讨论了布尔代数的(∈，∈∨q)-Fuzzy子代数在布尔代数同态下的像和逆像，并证明了当I是布尔代数R的(∈，∈∨q)-Fuzzy真理想时，R／I是布尔代数。2．基于对已有Fuzzy子代数和(∈，∈∨q)-Fuzzy子代数的讨论，提出了布尔代数的阈值Fuzzy子代数的概念，并讨论了其相关性质和两种Fuzzy子代数之间的关系。3．讨论了布尔代数的Fuzzy子代数的直积的一些性质，给出了直积布尔代数的Fuzzy子代数可分解为两个Fuzzy子代数的直积的充要条件，并讨论了Fuzzy商布尔代数的直积特征。4．运用mizar语言给出了布尔代数的Fuzzy子代数和(∈，∈∨q)-Fuzzy子代数的mizar定义，而且编写了一些相关重要结论和定理的程序，并使用mizar系统进行验证并通过。从而在mizar系统中实现了关于布尔代数的Fuzzy子代数的一些重要性质的证明。

关键词：布尔代数 (∈,∈∨q)-Fuzzy子代数阈值Fuzzy子代数 Fuzzy子代数的直积 mizar

函数微分、差分差商及连分数的mizar实现研究

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

函数微分、差分差商及连分数的Mizar实现研究

作者：张燕青岛科技大学

学位级别：硕士

mizar系统是从人工智能的一个分支——定理自动证明的发展过程中产生和发展起来的，是用来构建mizar数学知识库的证明校验系统，是一个数学定理证明工具。mizar系统由波兰华沙大学的Andrzej Trybulec教授组织的mizar协会领导，其逻辑框... 详细信息

mizar系统是从人工智能的一个分支——定理自动证明的发展过程中产生和发展起来的，是用来构建mizar数学知识库的证明校验系统，是一个数学定理证明工具。mizar系统由波兰华沙大学的Andrzej Trybulec教授组织的mizar协会领导，其逻辑框架基于Ja(?)kowski自然演绎推理的古典逻辑。mizar如今已经成为集逻辑证明、校验、排版功能于一体的数学知识处理的形式化系统，拥有自己的数据库MML，其中收录了波兰、日本、中国、加拿大等多个国家的教授学者和研究生完成的960多篇数学论文，几乎涵盖了数学的各个分支，尤其是在连续格的证明、Jordan曲线及Brouwer不动点等定理的证明中突显出mizar语言系统的优越性。本文首先介绍了定理机器证明及mizar系统的历史，其次对如何利用mizar语言完成数学论文和进行自动推理校验给出了简要的说明。本文主要研究了以mizar系统为平台，证明一类特殊函数的微分公式、函数的差分差商和实现任一实数的连分数形式。主要的创新点如下： 1．将mizar系统中的可微性判定及基本函数的性质定理应用于几类复合函数，实现了它们在mizar系统中的自动推理证明;2．为了实现函数的差分与差商，在mizar系统中首次定义了平移算子、向前差分算子、向后差分算子和中心差分算子，并由此定义了三种无穷差分序列forwardifference、backwardifference和centralifference，讨论了三者之间的相互关系，应用mizar语言完成了相关定理的自动推理证明，并验证其正确性;3．首创性地在mizar中定义了任一实数的连分数形式及其渐近分数，讨论了连分数及渐近分数分子、分母的有关性质，利用渐近分数的性质完成了任一实数的渐近分数的mizar实现，并给出证明其渐近性质的机械化方法。以上结果都通过了mizar系统的验证，均被收录到最新的mizar数据库MML中，并发表于2005和2006年的Formalized Mathematics期刊。

关键词： mizar 定理机器证明微分差分差商欧几里德算法连分数

双线性函数的度量矩阵及二次型在mizar语言下的实现

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

双线性函数的度量矩阵及二次型在Mizar语言下的实现

作者：刘玲玲青岛科技大学

学位级别：硕士

计算机的自动推理证明是数学与计算机科学相结合的一个新学科,随着计算机技术的高速发展,该学科也迅速发展,各种机器语言应运而生。利用机器语言编写程序,实现了数学问题在计算机上的证明。mizar语言就是其中一种。 mizar语言系统是... 详细信息

计算机的自动推理证明是数学与计算机科学相结合的一个新学科,随着计算机技术的高速发展,该学科也迅速发展,各种机器语言应运而生。利用机器语言编写程序,实现了数学问题在计算机上的证明。mizar语言就是其中一种。 mizar语言系统是用于证明或计算数学问题的计算机语言系统,在定理自动证明的发展过程中逐步完善。如今mizar已经成为集逻辑证明、自然演绎、复杂计算、校验排版、科研教学于一体的处理数学知识的形式化系统,拥有着世界上最大的数据库MML。本文简单介绍了mizar语言系统,并应用mizar语言系统对双线性函数的度量矩阵和二次型等问题给出相应的证明,主要工作如下: 1.定义出双线性函数的度量矩阵,利用度量矩阵进一步探讨双线性函数。 2.实现了对称双线性函数、反对称双线性函数、退化双线性函数和非退化双线性函数的定义,简单讨论了他们的度量矩阵及性质。 3.给出了二次型,正定二次型,正定矩阵等相关定义。

关键词： mizar 双线性函数度量矩阵二次型

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于mizar的函数奇偶性及周期性的研究

基于MIZAR的函数奇偶性及周期性的研究

作者：门艳红青岛科技大学

学位级别：硕士

数学问题机械化是指用计算机推理、证明、计算数学问题和定理。目前,世界各国都在积极地进行数学问题机械化的研究,比较著名的数学定理证明系统有mizar、PVS、Coq等,而mizar语言系统凭借其庞大的MML数据库和其优越的功能,得以快速发展,... 详细信息

数学问题机械化是指用计算机推理、证明、计算数学问题和定理。目前,世界各国都在积极地进行数学问题机械化的研究,比较著名的数学定理证明系统有mizar、PVS、Coq等,而mizar语言系统凭借其庞大的MML数据库和其优越的功能,得以快速发展,深受世界各国的重视。mizar语言系统已经发展成为集众多功能于一体的数学知识处理系统,目前MML数据库已经收录1090多篇数学论文,其内容几乎涵盖了数学的各个分支,尤其是在拓扑学及泛函分析学等学科的定理证明中更突显出mizar语言系统的优越性。本文首先介绍了mizar系统的发展历史,接着给出了奇函数、偶函数及周期函数的mizar定义,同时完成了奇函数、偶函数及周期函数的性质在mizar系统下的实现和论证。本文主要工作如下：1.给出了拟奇函数及拟偶函数的mizar系统下的定义,同时,在复数域上给出奇函数及偶函数的定义,将分析学中奇偶函数的定义加以推广并在mizar系统下实现;2.在mizar系统下给出了周期函数及周期的定义;3.基于mizar系统论证了奇函数、偶函数及周期函数的性质以及某些复合函数的奇偶性及周期性;4.在mizar系统下,证明了一些初等函数的奇偶性及周期性,例如：常函数、符号函数、绝对值函数及某些三角函数;5.进一步完善了mizar系统下符号函数的定义及性质的论证。以上结果都通过了mizar系统的验证,均被收录到最新的mizar数据库MML中并发表在Formalized Mathematics期刊。

关键词： mizar 机器证明奇函数偶函数周期函数

特殊函数差分差商积分及函数正交性与函数范数的mizar实现研究

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

特殊函数差分差商积分及函数正交性与函数范数的Mizar实现研究

作者：庄延平青岛科技大学

学位级别：硕士

从定理自动证明的发展过程中产生和发展起来的mizar系统,是用来构建mizar数学知识库的证明校验系统,也是一个数学定理证明工具。mizar系统的逻辑框架基于Jagkowski自然演绎推理的古典逻辑。mizar如今已经成为集逻辑证明、校验、排版功... 详细信息

从定理自动证明的发展过程中产生和发展起来的mizar系统,是用来构建mizar数学知识库的证明校验系统,也是一个数学定理证明工具。mizar系统的逻辑框架基于Jagkowski自然演绎推理的古典逻辑。mizar如今已经成为集逻辑证明、校验、排版功能于一体的数学知识处理的形式化系统,拥有自己的数据库MML,其中收录了一千多篇数学论文,几乎涵盖了数学科学的各个分支。本文首先介绍了定理机器证明及mizar系统的历史,其次对如何利用mizar语言完成数学论文和进行自动推理校验给出了简要的说明。本文主要研究了以mizar系统为平台,证明特殊函数的差分差商、特殊函数的积分和实现函数正交性与函数范数。本文主要的创新点如下:.1.完成了特殊函数的差分差商在mizar系统中的实现;2.根据特殊函数的微分公式及可积性,在mizar中实现多种特殊函数的积分;3.首次在mizar中定义了函数的正交性与函数范数,并讨论了有关性质,应用mizar语言完成了相关定理的自动推理证明,并验证其正确性。以上结果均通过mizar系统的验证,被收录到最新的mizar数据库(MML)中,并发表于2008年和2009年的Formalized Mathematics。

关键词： mizar 定理机器证明差分差商积分函数正交性函数范数

四元数混合运算及特殊函数的微分公式和洛尔定理应用的mizar实现

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

四元数混合运算及特殊函数的微分公式和洛尔定理应用的Mizar实现

作者：王攀青岛科技大学

学位级别：硕士

数学问题的机器证明是利用计算机证明和求解数学问题。mizar语言系统是上世纪八十年代开创的集逻辑证明、校验、排版功能于一体的计算机语言系统。如今该系统已拥有自身的数据库MML,收录了几乎涵盖数学各个分支的1000多篇数学论文。同时... 详细信息

数学问题的机器证明是利用计算机证明和求解数学问题。mizar语言系统是上世纪八十年代开创的集逻辑证明、校验、排版功能于一体的计算机语言系统。如今该系统已拥有自身的数据库MML,收录了几乎涵盖数学各个分支的1000多篇数学论文。同时,mizar语言系统在自动化控制、声音和图像识别等研究领域也有着广泛的应用。本文首先介绍了定理机器证明和mizar语言系统的发展历史,其次简单描述了mizar系统下定理机器证明和校验数学命题的方法,在此基础上对四元数的混合运算,特殊复合函数的微分以及洛尔定理的应用等方面进行了mizar实现。本文主要工作:1.在mizar系统中定义了有关四元数的几个概念,完成了四元数的混合运算性质的mizar实现,对于四元数模的一些相关命题也进行了一定的mizar论证。2.基于mizar数据库中已有的三角函数、幂函数、对数函数及可微性定理,成功地对一些特殊复合函数的微分进行了mizar实现。3.将mizar系统中已实现的洛尔定理与相关数学知识相结合,在mizar系统中实现了洛尔定理和柯西中值定理的一些应用和推广。以上结果均已通过mizar语言系统的验证,部分内容已被收录在mizar数据库MML中。

关键词：机器证明 mizar 四元数微分洛尔定理