Computer Proving Of Several Theorem In BCI-Algebra Ideals

Presently,the research in mathematics mechanization is becoming the leading edge of our country and the western developed countries.With the development of the research,we can invent many kinds of computer language to programming using mechanization method,and use them in mathematics mechanization. Internationally,the mathematician studying mathematics mechanization usually call it "formalize mathematics",and call the program of mathematics mechanization as "ormal mathematics language".Mathematical Knowledge Management(MKM) is a international mathematic organization studying "mathematics mechanization".This organization invent automated theorem proving systerm to prove mathematic knoledge using different computer language in such a global and international enviromen.In this way,mathematics can develop more quickly and get applicated more widely.Mizar systerm is a mathematics mechanization computer language systerm.It has its own edition language.Mizar language and the largest database in the world(MML).MML also has the on-line edition of the "Formalized Mathematics",we can look it up on the intemet.Now,Mizar symterm has becomes a collection of nature deduction,the complex computation,the automatic typesetting and the scientific research teaching.It is competitive and has a bright future.This paper discuss the comptter proving of several theorem in BCI-Algebra ideals in Mizar systerm,give the definition of p-ideals,associative ideals,quasiassociative ideals,commutative ideals,implicative ideals and positive implicative ideals,and discuss their properties in Mizar systerm.The closed ideals in Mizar systerm is also disussed.All the results above have been checked by the Mizar systerm and have been acceped by Mizar database(MML).Its text formatting has been published by "Formalized Mathematics "...