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

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

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

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