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

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

2、展著廣泛的合作交流。目前MML數(shù)據(jù)庫已經(jīng)收錄1010多篇數(shù)學(xué)論文，幾乎涵蓋了數(shù)學(xué)的各個分支，尤其是在連續(xù)格的證明、不同維數(shù)的Jordan曲線及拓?fù)鋵W(xué)、泛函分析學(xué)等定理的證明中更突顯出Mizar語言系統(tǒng)的優(yōu)越性。 本文首先介紹了Mizar系統(tǒng)的發(fā)展歷史及Mizar語言的使用方法，并在Mizar系統(tǒng)中，給出了實現(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)中的“＼”運算上，添加了新的“*”運算，構(gòu)成了有條件(S)的BCI-代數(shù)和BCK-代數(shù)，創(chuàng)新性地對BCI-代數(shù)的“＼”運算進(jìn)行了雙元右累次冪運算的Mizar定義，給出了擬可換BCI-代數(shù)和BCK-代數(shù)的Mizar實現(xiàn)，同時在Mizar系統(tǒng)中討論了上述所有的相關(guān)性質(zhì)，所做結(jié)論都通過了Mizar系統(tǒng)的驗證，均被收錄到最新的Mizar數(shù)據(jù)庫MML中，發(fā)表于2007和