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