Mizar语言的开发与应用

摘要

本文首先介绍了Mizar系统的历史及使用方法，然后给出了利用Mizar语言解决实系数和复系数一元二、三次方程的复数解、讨论了几类常用的特殊方程实数解的情况；其次利用Mizar语言解决了图像处理中经常用到的数学形态学的若干基本问题并给出了相应的算法。这些结果都通过了Mizar系统的验证并被收录到MML数据库中。

目录

文摘

英文文摘

1绪论

1.1 Mizar系统的概述

1.2 Mizar系统发展的历史和现状

1.2.1 1973-74开始阶段

1.2.2 1975 Mi zar-PC

1.2.3 1977：Mizar-QC/1204和Mizar-QC/6000

1.2.4 1977-1988年

1.2.5 1989至今

1.3本课题的目的和意义

1.4本论文的主要研究内容

2 MIZAR语言的简介

2.1 Mizar文章的剖析

2.2 Mizar基本语法结构

2.2.1数据类型

2.2.2数据项

2.2.3原子公式

2.2.4公式

2.3定理证明

2.3.1简单依据

2.3.2证明方法

2.3.3数据类型的改变

2.3.4一些惯例

2.3.5连等于的使用

2.3.6扩散陈述

2.3.7模式

2.4定义

2.4.1词汇表文件的书写方法

2.4.2变量的定义

2.4.3结构的定义

2.4.4 Mode的定义

2.4.5属性的定义

2.4.6 Cluster的定义

2.4.7谓词的定义

2.4.8函数的定义

2.4.9重定义

3 MIZAR数据库与系统

3.1 Mizar数据库

3.2 Mizar系统

4开发应用之实系数复系数方程的复数解

4.1环境部的设置

4.2正文

5开发应用之数学形态学

5.1数学形态学的基本知识

5.2二值图像数学形态学的实现

5.2.1简介

5.2.2 MIZAR实现

6总结与展望

参考文献

致谢

攻读学位期间发表的学术论文目录：