BCL-代數和BCK-代數的代數結構在Mizar系統(tǒng)中的實現.pdf

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

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

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