Mizar語言系統(tǒng)與四元數(shù)的代數(shù)結(jié)構(gòu).pdf

1、計(jì)算機(jī)證明數(shù)學(xué)問題是當(dāng)今世界積極研究的一個(gè)熱門領(lǐng)域。迄今為止，世界已有多種可用來進(jìn)行數(shù)學(xué)命題證明和邏輯推理的機(jī)器語言系統(tǒng)，但其中只有少數(shù)幾種語言可被普遍接受并受到數(shù)學(xué)家與計(jì)算機(jī)專家的認(rèn)可，如HOL、Mizar、PVS、Coq等，它們各自的初衷不同，卻有一個(gè)共同的特征：人類使用機(jī)器語言書寫、計(jì)算、邏輯推理和證明文本性質(zhì)的數(shù)學(xué)問題，并由計(jì)算機(jī)自動(dòng)驗(yàn)證其正確性。這里討論的Mizar系統(tǒng)是由波蘭Hock科學(xué)協(xié)會(huì)的Andrzej Trybulec

2、教授領(lǐng)導(dǎo)下開發(fā)的。經(jīng)過近30年的發(fā)展，Mizar系統(tǒng)已經(jīng)形成了著名的數(shù)學(xué)知識(shí)處理的形式化系統(tǒng)。在此系統(tǒng)下，完成了大量的數(shù)學(xué)問題的計(jì)算機(jī)證明。這些數(shù)學(xué)知識(shí)涵蓋了幾乎數(shù)學(xué)的每一個(gè)分支，解決了人們用手無法計(jì)算和證明的一些復(fù)雜問題。同時(shí)，它在自動(dòng)控制、聲音和圖像識(shí)別等研究領(lǐng)域有著廣泛的應(yīng)用，為今后討論數(shù)學(xué)及其相關(guān)學(xué)科奠定了一個(gè)良好的基礎(chǔ)。 本文首先介紹了Miear系統(tǒng)的計(jì)算機(jī)操作原理和使用方法，給出了在Mizar語言系統(tǒng)下四元數(shù)、四元數(shù)