当前，世界各国都在积极地进行数学问题的计算机辅助证明的研究，比较著名的数学定理证明验证系统有Mizar、PVS、Coq等，而Mizar语言系统更依靠其庞大的MML数据库及新颖的“人机对话”功能，得到了迅速地发展，并受到广泛的重视和研究应用。如今，Mlizar系统已经发展成为集自然演绎、逻辑证明、复杂计算、科研教学、自动排版功能于一体的数学知识处理的形式化系统，由波兰华沙大学发起的Mizar协会主持，并与中国、日本、加拿大、俄罗斯等国家开展着广泛的合作交流。目前MML数据库已经收录1010多篇数学论文，几乎涵盖了数学的各个分支，尤其是在连续格的证明、不同维数的Jordan曲线及拓扑学、泛函分析学等定理的证明中更突显出Mizar语言系统的优越性。 本文首先介绍了Mizar系统的发展历史及Mizar语言的使用方法，并在Mizar系统中，给出了实现BCI-代数和BCK-代数的代数结构的方法，构建p-半单的BCI-代数、结合的BCI-代数和可换的、关联的以及正定关联的BCI-代数和BCK-代数的方法，尝试性地通过Mizar在原有的BCI-代数结构中的“＼”运算上，添加了新的“*”运算，构成了有条件(S)的BCI-代数和BCK-代数，创新性地对BCI-代数的“＼”运算进行了双元右累次幂运算的Mizar定义，给出了拟可换BCI-代数和BCK-代数的Mizar实现，同时在Mizar系统中讨论了上述所有的相关性质，所做结论都通过了Mizar系统的验证，均被收录到最新的Mizar数据库MML中，发表于2007和2008年的FormalizedMathematics期刊。 在此研究领域，作者在导师的指导下，在《FormalizedMathematics》杂志上已发表了4篇论文，详见71页。