数学文化课程论文_数学文化结课论文

数学文化课程论文由刀豆文库小编整理，希望给你工作、学习、生活带来方便，猜你可能喜欢“数学文化结课论文”。

浅谈数学机械化

一、数学机械化的概念 何为数学机械化？所谓数学问题的机械化,就是要求在运算或证明过程中，每前进一步之后，都有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。即将数学的主要内容，方程求解与定理证明，转变为计算机可以接受的形式并利用计算机强大的计算功能解决数学与高新技术中的理论问题。即所谓的机械化就是刻板化和规格化，也就是对一类定理(可以是成千上万)提供一种统一的算法，使得该类定理中的每个定理，都可依此方法给出证明。从而实现从“一理一证”到“一类一证”的飞跃。在数学中，要通过推理和证明来建立定理，证明的每一个步骤都是通过逻辑推理，推出另一些命题。从它们出发进行推理的命题称为前提，由此推出的命题称为结论。而机器证明，就是要把这项推理和证明的工作交由计算机去完成。它是现代数学中一种新兴的边缘性学科，是现代人工智能发展的一个重要方向。

二、数学机械化的理论基础

数学机械化研究，是在初等几何定理的机器证明研究方面取得突破的。公理化体系的几何定理证明非常不机械化。以中学课程中的几何为例，－个定理的证明，往往要经过冥思苦想，奇巧构思，无章可循地填加辅助线，迂回曲拆地给出证明。如何利用计算机进行自动惟理，特别是进行几何定理的自动证明，是学术界长期研究的课题。所谓定理的机械化证明，就是对一类定理（这类定理可能成千上万）提供一种统一的方法，使得该类定理中每个定理，都可依此方法给出证明。在证明过程中，每前进一步，都有章可循地确定下一步该做什么和如何做。从“一理一证”到“－类一证”，是数学的认识和实践的飞跃。吴先生创立了初等几何（泛指不具有微分运算的几何，如欧氏几何、非欧几何、仿射几何、投影几何、代数几何等等）定理证明的机械化方法，国际上称“吴方法”，首次实现了高效的几何定理的机器证明。“吴方法”也可用于几何定理的自动发现和未知关系的自动推导。吴文俊先生的开创性成果，打破了国际自动推理界在几何定理自动证明研究中长期徘徊不前的局面，也使我国在这一领域处于领先地位。吴先生的杰出贡献，使他获得1998年度国际自动推理界的最高奖“Herbrand奖”。

例如机械化证明几何定理：首先引进坐标，使待证定理的假设与终结都转换成多项式方程。这在通常的情形都是如此的。然后依照某种确定的方式对代表假设的多项式方程进行处理，使在有限步骤后到达代表结论的那一个多项式方程，或与之相反。这就给出了一个机械地进行的证明或否定一个几何定理的过程。这一方法还具有普适的性质。即不论所考虑的定理出自何种初等几何，不论是欧氏的，还是非欧的，只要像通常出现的那样，假设与终结都可用多项式方程来表示，就可应用这同一的方法与过程

三、数学机械化的发展历程

历史上一些大师级的数学家，曾在几何定理的机器证明这条道路上艰辛地探索过。笛卡儿为了用代数的方法来处理千变万化的几何问题，发明了坐标方法，创立了解析几何，这是科学上的一件大事，从而为用计算机解决几何问题打下了基础。

莱布尼滋，微积分的创始人之一，曾有过“推理机器”的设想。他还提出了现代计算机上所用二进制记数法，这项工作促进了数理逻辑的早期工作。

大数学家希尔伯特在他的《几何基础》中，曾给出了一类几何问题的机械化解题方法。9 4 5年，波兰数理逻辑学家塔尔斯基(A．A．Tarski)证明了一个值得称道的定理——塔尔斯基定理：一切初等几何和初等代数的命题，都可以机器证明。(前提和结论都可以用有限个整系数多项式的等式或不等式来表达的命题，叫做初等几何和初等代数命题。)1 9 7 5年，考林斯(Collins)提出了“柱面代数分解方法”，比塔尔斯基的方法提高了许多，但在计算机上仍然只能解决个别稍难点的几何问题。

20世纪70年代以来，吴文俊研究机器证明问题。他提出的机械化方法，国际上称之为“吴方法”，被认为是机器证明的里程碑式的贡献。2001年，吴文俊获首届中国国家最高科技奖，而机器证明是获奖的主要原因。

1984年，吴文俊院士的学术专著《集合定理机器证明的基本原理(初等几何部分)》由科学出版社出版。这本专著遵循机械化思想引进数系和公理，依照机械化观点系统地分析了各类几何体系，诸如Pascal几何、垂直几何、度量几何，以及欧氏几何，证明确立了各类几何的机械化定理，系统地阐明了几何定理机器证明代数方法的基本原理。

后来，洪加威等人提出了通过数值实例的检验（即列举法）来证明几何定理的思

想方法，张景中、杨路提出了数值并行法和面积法，李洪波、王车明发展了不变量方法，极大地促进了数学机械化的发展。

四、数学机械化的应用

1.证明几何学问题

几何学包括定理证明、几何作图和几何不等式证明。在吴先生开刨性成果的影响和启迪下，在几何学的机械化方面，如定理机器证明、几何自动作图和几何不等式机器证明，我国学者都取得了很大成绩。

众所周知，直线和平面等几何概念可由一次代数方程描述，多项式方程则用于描

述曲线和曲面等。数学科学中，从线性到非线性的第一步跨跃，是由多项式实观的。因此，多项式方程组求解是非线性数学最基本的课题，这个问题的研究已经持续几百年。数学不同分支中许多的问题、自然科学不同领域中很多的问题、高新技术中大量的问题，都可转化为多项式方程组求解。在几何定理机器证明的过程中，必须理清多项式方程组的零点结构。这一需求，促使吴先生创立了多项式方程组求解的理论和方法，国际上称“特征列法”或“吴消元法”。吴先生还把这些方法拓展到微分情形，建立了微分几何定理机器证明和微分代数方程组求解的机械化理论和方法。自然，较之代数情形，微分代数的应用范围更为广阔，同时，问题的研究更为复杂和困难。

2.四色问题的证明

人工智能定理证明最有说服力的例子，是机器证明了困扰数学界长达100余年之久的难题——“四色定理”。据说，“四色问题”最早是1852年一位21岁的大学生提出的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。这个看似简单的问题，就象“哥德巴赫猜想”一样，不知难倒了多少著名数学家和献身数学的业余爱好者，属于世界上最著名的数学难题之一。

1976年6月，美国伊利诺斯大学的两位数学家沃尔夫冈·哈肯（W.Haken）和肯尼斯·阿佩尔（K.Apple）自豪地宣布，他们用电脑证明了这一定理。哈肯和阿佩尔攻克这一难题使用的方法仍然是前人提出的“穷举归纳法”，只是别人用的是手工计算，无论如何也不能“穷举”所有的可能性。哈肯和阿佩尔编制出一种很复杂的程序，让3台

IBM360大型电脑去自动高速寻找各种可能的情况，并逐一判断它们是否可以被“归纳”。十几天后，共耗费了1200个机时，做完了200亿个逻辑判断，电脑终于证明了“四色定理”。

3.数学定理的自动发现

数学机械化的发展方向不仅仅是定理自动证明，它还应该能使用户发现他以前并不知道的定理，即定理的自动发现或猜想的自动提出。

以HR系统为例，来阐述如何自动发现定理。

HR系统是一种主要做描述性归纳工作的机器学习系统，它能基于所给的背景知识提出经验性的猜想，并尝试使用第三方软件来证明该猜想的正确性。下面我们把该系统所能做的工作分为6大类：（ⅰ）使用由用户提供的背景信息（ⅱ）发明新的概念（ⅲ）提出经验性猜想（ⅳ）寻找反例（ⅴ）证明该定理（ⅵ）报告结果。

计算技术在纯数学领域一个最要的应用就是使用CAS进行数学家无法通过手工完成的计算工作，在计算过程中通过对由CAS内部产生数据的分析来探索新的函数和提出经验性猜想。在该探索和发现过程中，我们通过使用HR系统提出关于用户所给的Maple函数的猜想，使这个探索和发现过程完全机械化。在该过程中，HR先用用户所提供的Maple函数的信息来发明新的概念，进而提出与这些新概念相关的数学猜想，然后把这个猜想交给第三方定理证明机，通常是Otter theorem prover, 来证明该猜想的真伪。这种方法已经成功运用在20多个有限代数理论体系中，其中主要包括数论、图论、集合理论和ring理论，发现了很多重要的新定理。

五、数学机械化的发展前景

自20世纪70年代以来，计算机解几何问题的本领已飞跃提高。但是更难的问题的解决，要求发展更有力的新方法。发展非线性代数方程组的并行插值求解方法，综合不同方法的长处以建立有效的人机交互求解系统，都是极有希望的研究方向。对于几何不等式和几何作图的机器求解的研究，这不但有传统的兴趣，更有广泛的应用，是目前国际上一个很活跃的领域。这一方向方兴未艾，有大量的工作可做。在几何定理的机器证明的各种方法都有长足的发展，如何把不同的方法综合起来，组织成有效的几何问题计算机自动求解或人机交互求解系统，将成为更有意义的研究方向。

在研究几何定理机器求解时，创造或发展了一些新的方法或代数工具，它们也可以用来解决其他领域的问题。如机构设计、曲面造型、计算机辅助设计、机器人控制、计算机视觉、自动控制、化学平衡、几何模型等领域都有着广泛的应用。但这些都是本领域人员自己的设想，与技术领域的实际需求有一定的距离。因此，有必要做更具体的分析，并开发界面友好、易学易用的软件。另一种应用是把几何定理机器证明的程序发展成软件，或者直接嵌入计算机应用软件中。在这些方面，数学机械化有很大的发展前景。

【参考文献】

[1] 吴文俊 《论数学机械化》 山东教育出版社1996年7月

[2] 易南轩，王芝平 《多远视角下的数学文化》 科学出版社 2007年9月

[3] 林东岱《数学与数学机械化》 山东教育出版社 2001