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

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

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