BCL-代數(shù)和BCK-代數(shù)的代數(shù)結(jié)構(gòu)在Mizar系統(tǒng)中的實(shí)現(xiàn).pdf

1、當(dāng)前，世界各國(guó)都在積極地進(jìn)行數(shù)學(xué)問題的計(jì)算機(jī)輔助證明的研究，比較著名的數(shù)學(xué)定理證明驗(yàn)證系統(tǒng)有Mizar、PVS、Coq等，而Mizar語(yǔ)言系統(tǒng)更依靠其龐大的MML數(shù)據(jù)庫(kù)及新穎的“人機(jī)對(duì)話”功能，得到了迅速地發(fā)展，并受到廣泛的重視和研究應(yīng)用。如今，Mlizar系統(tǒng)已經(jīng)發(fā)展成為集自然演繹、邏輯證明、復(fù)雜計(jì)算、科研教學(xué)、自動(dòng)排版功能于一體的數(shù)學(xué)知識(shí)處理的形式化系統(tǒng)，由波蘭華沙大學(xué)發(fā)起的Mizar協(xié)會(huì)主持，并與中國(guó)、日本、加拿大、俄羅斯等國(guó)家開

2、展著廣泛的合作交流。目前MML數(shù)據(jù)庫(kù)已經(jīng)收錄1010多篇數(shù)學(xué)論文，幾乎涵蓋了數(shù)學(xué)的各個(gè)分支，尤其是在連續(xù)格的證明、不同維數(shù)的Jordan曲線及拓?fù)鋵W(xué)、泛函分析學(xué)等定理的證明中更突顯出Mizar語(yǔ)言系統(tǒng)的優(yōu)越性。 本文首先介紹了Mizar系統(tǒng)的發(fā)展歷史及Mizar語(yǔ)言的使用方法，并在Mizar系統(tǒng)中，給出了實(shí)現(xiàn)BCI-代數(shù)和BCK-代數(shù)的代數(shù)結(jié)構(gòu)的方法，構(gòu)建p-半單的BCI-代數(shù)、結(jié)合的BCI-代數(shù)和可換的、關(guān)聯(lián)的以及正定關(guān)聯(lián)的B

3、CI-代數(shù)和BCK-代數(shù)的方法，嘗試性地通過Mizar在原有的BCI-代數(shù)結(jié)構(gòu)中的“＼”運(yùn)算上，添加了新的“*”運(yùn)算，構(gòu)成了有條件(S)的BCI-代數(shù)和BCK-代數(shù)，創(chuàng)新性地對(duì)BCI-代數(shù)的“＼”運(yùn)算進(jìn)行了雙元右累次冪運(yùn)算的Mizar定義，給出了擬可換BCI-代數(shù)和BCK-代數(shù)的Mizar實(shí)現(xiàn)，同時(shí)在Mizar系統(tǒng)中討論了上述所有的相關(guān)性質(zhì)，所做結(jié)論都通過了Mizar系統(tǒng)的驗(yàn)證，均被收錄到最新的Mizar數(shù)據(jù)庫(kù)MML中，發(fā)表于2007和