学位论文 > 优秀研究生学位论文题录展示

Mizar语言系统与四元数的代数结构

作　者: 葛夫国
导　师: 梁希泉
学　校: 青岛科技大学
专　业: 应用数学
关键词: 计算机数学问题 Mizar系统四元数代数结构
分类号: O153
类　型: 硕士论文
年　份: 2007年
下　载: 31次
引　用: 1次
阅　读: 论文下载

内容摘要

计算机证明数学问题是当今世界积极研究的一个热门领域。迄今为止，世界已有多种可用来进行数学命题证明和逻辑推理的机器语言系统，但其中只有少数几种语言可被普遍接受并受到数学家与计算机专家的认可，如HOL、Mizar、PVS、Coq等，它们各自的初衷不同，却有一个共同的特征：人类使用机器语言书写、计算、逻辑推理和证明文本性质的数学问题，并由计算机自动验证其正确性。我们这里讨论的Mizar系统是由波兰Plock科学协会的Andrzej Trybulec教授领导下开发的。经过近30年的发展，Mizar系统已经形成了著名的数学知识处理的形式化系统。在此系统下，完成了大量的数学问题的计算机证明。这些数学知识涵盖了几乎数学的每一个分支，解决了人们用手无法计算和证明的一些复杂问题。同时，它在自动控制、声音和图像识别等研究领域有着广泛的应用，为今后讨论数学及其相关学科奠定了一个良好的基础。本文首先介绍了Mizar系统的计算机操作原理和使用方法，给出了在Mizar语言系统下四元数、四元数的运算、共轭、内积、模等代数结构理论的证明，所做结论都通过了Mizar系统的验证，发表在波兰的《Formalized Mathematics》杂志上，并被收录到MML(Mizar Mathematical Library)数据库中。在此研究领域，作者在导师的指导下，在《Formalized Mathematics》杂志上已发表了5篇论文，详见网站http://www.mizar.org/fm／。

全文目录

摘要  3-4
Abstract  4-9
1 绪论  9-13
  1.1 数学命题的机械化证明的历史  9-10
  1.2 国内外研究动态  10-11
  1.3 Mizar系统的历史发展过程及现状  11-13
    1.3.1 Mizar系统概述  11
    1.3.2 Mizar系统的发展历史  11-13
  1.4 本文内容及安排  13
2 Mizsr系统简介  13-26
  2.1 Mizar论文结构  13-15
  2.2 Mizar语言的基本语法结构  15-16
    2.2.1 Mizar语言的数据类型  15
    2.2.2 Mizar语言的公式  15-16
  2.3 定理证明的方法  16-21
    2.3.1 简单依据  16
    2.3.2 证明方法  16-19
    2.3.3 数据类型的改变  19
    2.3.4 一些惯例  19-20
    2.3.5 连等于的使用  20-21
    2.3.6 扩散陈述  21
    2.3.7 模式  21
  2.4 定义  21-26
    2.4.1 词汇表文件的书写方法  21-23
    2.4.2 结构的定义  23
    2.4.3 mode的定义  23-24
    2.4.4 属性(attr)的定义  24
    2.4.5 cluster的定义  24
    2.4.6 谓词的定义  24-25
    2.4.7 函数的定义  25
    2.4.8 重定义  25-26
3 Mizsr数据库与系统  26-28
  3.1 Mizar数据库  26
  3.2 Mizar系统  26-27
  3.3 Mizar系统的安装  27
  3.4 Mizar系统中常用的几个命令  27-28
4 四元数及其性质在Mizar语言系统上的实现  28-66
  4.1 四元数的基本知识  28-37
    4.1.1 四元数的发现及应用  28-29
    4.1.2 四元数的定义、四元数的运算  29-32
    4.1.3 四元数的复数表示和相似关系  32-34
    4.1.4 四元数体  34
    4.1.5 四元数矩阵  34-37
  4.2 四元数、四元数的运算、模、共轭、内积及相关性质在Mizar系统上的实现  37-43
    4.2.1 环境部的设置和变量的声明  37-38
    4.2.2 四元数的定义  38-39
    4.2.3 虚数单位i,j,k在计算机上的定义  39-42
    4.2.4 如何让系统识别新定义的四元数数据类型  42
    4.2.5 四元数在计算机上的表示  42-43
  4.3 四元数的运算在Mizar系统上的实现  43-50
    4.3.1.四元数的加法  43-45
    4.3.2 四元书的相反数  45-46
    4.3.3 四元数的减法  46
    4.3.4 四元数的乘法  46-47
    4.3.5 四元数的除法  47-49
    4.3.6 四元数的逆  49
    4.3.7 虚数单位i,j,k在计算机上的表示  49-50
  4.4 实部和虚部的定义  50-55
  4.5 零元素和单位元  55-56
  4.6 一个重要定理的证明  56-58
  4.7 四元数运算的另一种表示  58-62
    4.7.1 四元数的加法  58
    4.7.2 四元数的相反数  58
    4.7.3 四元数的减法  58-59
    4.7.4 四元数的乘法  59-60
    4.7.5 四元数的除法  60-61
    4.7.6 四元数的逆  61-62
  4.8 四元数的共轭  62-63
  4.9 四元数的模  63-64
  4.10 四元数的内积  64-65
  4.11 最终实现的Mizar形式  65-66
5 四元数的代数结构在Mizar语言系统里的实现  66-75
  5.1 代数结构的组成与四元数的二元运算  66-67
  5.2 四元数群的代数结构的定义和证明  67-70
  5.3 四元数环的代数结构的定义和证明  70-72
  5.4 相关定理的证明  72-73
  5.5 四元数环中元素的共轭与模  73-74
  5.6 最终实现的Mizar形式  74-75
总结与展望  75-77
参考文献  77-80
致谢  80-81
攻读学位期间发表(完成)的学术论文目录  81-82

Mizar语言系统与四元数的代数结构

内容摘要

全文目录

相似论文