积分商城

最新搜索： ide手册 WINCE 传感器 拼音输入 STM32CubeMX vee使用
您现在的位置是：首页 > 技术资料 > BCI代数理想问题的计算机证明
推荐星级：
  • 1
  • 2
  • 3
  • 4
  • 5

BCI代数理想问题的计算机证明

更新时间：2019-11-14 23:19:22 大小：13M 上传用户：sun2152查看TA发布的资源 标签：bci 下载积分：0分 评价赚积分 （如何评价?） 打赏 收藏 评论(0) 举报

资料介绍

当前，数学机械化已经成为我国和西方发达国家积极研究的前沿领域。随着研究的进一步深入，人们已经能够根据机械化方法创建各种机器语言来编写证明和计算程序，并在计算机上给出数学定理的证明或复杂计算。数学家们通常把“数学机械化”称为数学形式化，把“实现数学机械化的程序”称为形式化的数学语言。北美数学知识管理组织就是致力于“数学机械化”的一个国际化的数学组织。它在一个宏观的、国际化的环境中，通过创建定理自动推理系统，让数学知识在不同的机器语言程序中相互转换和交叉发展，从而使得核心数学及其应用更广泛、更迅速地发展。

Mizar 系统是一个用来证明数学问题的计算机语言系统，它拥有自己的编辑语言—Mizar语言和世界上最大的数学数据库（MML），同时MML也有期刊Formalized Mathematics的网页版本，在Intermet上可随时查阅，现在Mizar系统可以实现自然演绎、复杂计算、验证排版、科研教学一体化，具有很强的生命力和发展前景。本文主要在Mizar计算机语言系统的运行环境下，讨论BCI-

代数的理想问题，在Mizar系统中完成了p-理想，结合理想，拟结合理想，可换理想，关联理想和正定关联理想的定义以及相关的一些性质和定理。同时，本文也在Mizar系统中讨论了闭理想的一些性质的实现方法。本文利用Mizar语言给出了以上问题在计算机中的实现和证明，已得结果被收录到Mizar 数据库（MML）中，论文的文本形式已经在Formalized Mathematics杂志上表。


部分文件列表

文件名 大小
BCI代数理想问题的计算机证明.pdf 13M

【关注B站账户领20积分】

相关下载

全部评论(0)

暂无评论
评论赚积分>>

上传资源 上传优质资源有赏金

热门标签

更多>>

最新上传

  • 打赏
  • 30日榜单

热门下载

资料专题

推荐下载

本站上的所有资源均为源于网上收集或者由用户自行上传，仅供学习和研究使用，无任何商业目的，版权归原作如有侵权，请 来信指出，本站将立即改正。

ICP许可证号：京ICP证070360号     21IC电子网 2000- 版权所有

京ICP备11013301号

京公网安备 11010802024343号