- 1
- 2
- 3
- 4
- 5
BCI代数理想问题的计算机证明
资料介绍
当前，数学机械化已经成为我国和西方发达国家积极研究的前沿领域。随着研究的进一步深入，人们已经能够根据机械化方法创建各种机器语言来编写证明和计算程序，并在计算机上给出数学定理的证明或复杂计算。数学家们通常把“数学机械化”称为数学形式化，把“实现数学机械化的程序”称为形式化的数学语言。北美数学知识管理组织就是致力于“数学机械化”的一个国际化的数学组织。它在一个宏观的、国际化的环境中，通过创建定理自动推理系统，让数学知识在不同的机器语言程序中相互转换和交叉发展，从而使得核心数学及其应用更广泛、更迅速地发展。
Mizar 系统是一个用来证明数学问题的计算机语言系统，它拥有自己的编辑语言—Mizar语言和世界上最大的数学数据库（MML），同时MML也有期刊Formalized Mathematics的网页版本，在Intermet上可随时查阅，现在Mizar系统可以实现自然演绎、复杂计算、验证排版、科研教学一体化，具有很强的生命力和发展前景。本文主要在Mizar计算机语言系统的运行环境下，讨论BCI-
代数的理想问题，在Mizar系统中完成了p-理想，结合理想，拟结合理想，可换理想，关联理想和正定关联理想的定义以及相关的一些性质和定理。同时，本文也在Mizar系统中讨论了闭理想的一些性质的实现方法。本文利用Mizar语言给出了以上问题在计算机中的实现和证明，已得结果被收录到Mizar 数据库（MML）中，论文的文本形式已经在Formalized Mathematics杂志上表。
部分文件列表
| 文件名 | 大小 |
| BCI代数理想问题的计算机证明.pdf | 13M |
最新上传
- 打赏
- 30日榜单
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic下载 打赏310.00元 3天前
用户：小猫做电路
-
21ic下载 打赏310.00元 3天前
用户：gsy幸运
-
21ic下载 打赏310.00元 3天前
用户：liqiang9090
-
21ic下载 打赏310.00元 3天前
用户：zhengdai
-
21ic下载 打赏160.00元 3天前
用户：w1966891335
-
21ic下载 打赏160.00元 3天前
用户：w178191520
-
21ic下载 打赏160.00元 3天前
用户：kk1957135547
-
21ic下载 打赏40.00元 3天前
用户：WK520077778
-
21ic下载 打赏40.00元 3天前
用户：sun2152
-
21ic下载 打赏30.00元 3天前
用户：xuzhen1
-
21ic下载 打赏50.00元 3天前
用户：铁蛋锅
-
21ic下载 打赏30.00元 3天前
用户：xzxbybd
-
21ic下载 打赏40.00元 3天前
用户：z00
-
21ic下载 打赏40.00元 3天前
用户：forgot
-
21ic下载 打赏40.00元 3天前
用户：happypcb
-
21ic下载 打赏20.00元 3天前
用户：zhaoqshan
-
21ic下载 打赏5.00元 3天前
用户：17724187683
-
21ic下载 打赏5.00元 3天前
用户：zmm1818
-
21ic小能手 打赏15.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
chenruiji 打赏1.00元 3天前
资料：血糖仪原理图
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
资料：测试智能语音控制模块
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
cai0603 打赏3.00元 3天前
用户：CJQ_ENJOY
-
21ic小能手 打赏5.00元 3天前
全部评论(0)