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

摘要

当前，数学机械化已经成为我国和西方发达国家积极研究的前沿领域。随着研究的进一步深入，人们已经能够根据机械化方法创建各种机器语言来编写证明和计算程序，并在计算机上给出数学定理的证明或复杂计算。数学家们通常把“数学机械化”称为数学形式化，把“实现数学机械化的程序”称为形式化的数学语言。北美数学知识管理组织就是致力于“数学机械化”的一个国际化的数学组织。它在一个宏观的、国际化的环境中，通过创建定理自动推理系统，让数学知识在不同的机器语言程序中相互转换和交叉发展，从而使得核心数学及其应用更广泛、更迅速地发展。 Mizar系统是一个用来证明数学问题的计算机语言系统，它拥有自己的编辑语言—Mizar语言和世界上最大的数学数据库(MML)，同时MML也有期刊FormalizedMathematics的网页版本，在Internet上可随时查阅，现在Mizar系统可以实现自然演绎、复杂计算、验证排版、科研教学一体化，具有很强的生命力和发展前景。 本文主要在Mizar计算机语言系统的运行环境下，讨论BCI—代数的理想问题，在Mizar系统中完成了p—理想，结合理想，拟结合理想，可换理想，关联理想和正定关联理想的定义以及相关的一些性质和定理。同时，本文也在Mizar系统中讨论了闭理想的一些性质的实现方法。本文利用Mizar语言给出了以上问题在计算机中的实现和证明，已得结果被收录到Mizar数据库(MML)中，论文的文本形式已经在FormalizedMathematics杂志上表。

目录

文摘

英文文摘

声明

1绪论

1.1数学机械化的发展过程

1.2 Mizar系统的历史和发展现状

1.3课题研究的目的和意义

1.4课题研究的主要内容

2 Mizar语言

2.1 Mizar系统的安装

2.2 Mizar文章结构

2.3 Mizar语言的基本符号和语法词汇

2.3.1基本符号

2.3.2基本语法词汇

2.4 Mizar语言的证明方法

2.4.1 Mizar语言的一般表述与证明格式

2.4.2基本证明方法

2.5 Mizar语言系统中的定义(Definition)

2.6 Mizar中的逻辑推理检验及优化命令

2.7 Mizar系统的人机对话功能

3 BCI-代数理想的Mizar实现

3.1 BCI-代数理想

3.2 BCI-代数理想的Mizar实现

4几类特殊BCI理想的定义

4.1 p-理想定义的Mizar实现

4.2结合理想定义的Mizar实现

4.3可换理想定义的Mizar实现

4.4关联理想及正定关联理想定义的Mizar实现

5 几类特殊BCI理想的性质

5.1 p-理想的相关性质定理的Mizar实现

5.2结合理想及拟结合理想的相关性质定理的Mizar实现

5.2.1结合理想的相关性质的Mizar实现

5.2.2拟结合理想的相关性质的Mizar实现

5.3可换理想相关性质定理的Mizar实现

5.4关联理想及正定关联理想的相关性质定理的Mizar实现

5.5闭理想相关性质的Mizar实现

5.6最终实现的Mizar形式

结论与展望

参考文献

致谢

攻读学位期间发表(完成)的学术论文目录