几何定理机器证明的基本原理

出版时间：1984-8  出版社：科学出版社  作者：吴文俊  页数：234  字数：295000  
Tag标签：无  

内容概要

本书论述初等几何机器证明的基本原理，证明了奠基于各种公理系统的各种初等几何，只需相当于乘法交换律的某一公理成立，大都可以机械化。因此在理论上，这些几何的定理证明可以借助于计算机来实施。可以机械化的几何包括了多种有序或无序的常用几何、投影几何、非欧几何与圆几何等。     全书共分六章。前两章是关于几何机械化的预备知识，集中介绍了常用几何；后四章致力于几何的机械化问题。第3章为几何定理证明的机械化与Hilben机械化定理，第4，5章分别为（常用）无序几何的机械化定理和（常用）有序几何的机械化定理，第6章阐述各种几何的机械化定理。     本书可供数学工作者和计算机科学工作者以及高等院校有关专业的师生参考。

书籍目录

导言第1章  Desargues几何与Desargues数系    1.1  常用几何的Hilbert公理系统    1.2  无限公理与Desargues公理    1.3  Desargues平面中的有理点    1.4  Desargues数系与有理数子系    1.5  直线上的Desargues数系    1.6  Desargues平面的附属Desargues数系    1.7  Desargues平面几何的坐标系第2章  垂直几何、度量几何与常用几何    2.1  Pascal公理与乘法交换公理——（无序）Dascal几何    2.2  垂直公理与（无序）垂直几何    2.3  （无序）垂直几何的垂直坐标    2.4  （无序）度量几何    2.5  次序公理与有序度量几何    2.6  常用几何及其关属几何第3章  几何定理证明的机械化与Hilbert机械化定理    3.1  欧几里得证明方法小议    3.2  几何概念坐标表示的标准化    3.3  定理证明的机械化与mlbert关于Pascal几何中交点定理的机械化定理    3.4  Hilbert机械化证法举例    3.5  Hilbert机械化定理的证明第4章  （常用）无序几何的机械化定理    4.1  概述    4.2  多项式的因子分解    4.3  多项式组的整序    4.4  代数簇的构造性理论——一不可约升列与不可约代数簇    4.5  代数簇的构造性理论——代数簇的不可约分解    4.6  代数簇的构造性理论——维数概念与维数定理    4.7  无序几何机械化定理的证明    4.8  无序几何机械化证法举例第5章  （常用）有序几何的机械化定理    5.1  有序几何定理证明机械化概述    5.2  Tarski定理与Seidenberg方法    5.3  有序几何定理机械化证法举例第6章  各种几何的机械化定理    6.1  概述    6.2  投影几何定理证明的机械化    6.3  Bolyai—Lobachevsky双盐型非欧几何定理证明的机械化    6.4  Riemann椭圆型非欧几何定理证明的机械化    6.5  两种圆几何学定理证明的机械化    6.6  超越函数公式证明的机械化参考文献

章节摘录

　　1.1 常用几何的Hilbert公理系统　　本书所称常用几何，也就是通常的欧几里得几何。　　Hilbert的名著《几何基础》第一次为常用几何提出了一个完整的公理系统，使常用几何从此有了一个真正严实的基础。Hilbert的公理系统以一些不必要给以定义的基本概念作为讨论的目标。这些基本概念分成两类——基本对象，即点、直线以及平面；这些对象间的基本关系，即属于、介于以及全合于。它们服从若干公理，并作为逻辑推理的出发点。Hilbert把这些公理分成了五大类，构成了足以完全地刻画常用几何的一个完备的公理系统。这五类公理的名称如下：HI关联公理（从属公理）H11次序公理HIII全合公理HIV平行公理HV连续公理Hilbert的主要目的在于对空间直观给以系统的逻辑分析。为此，他详尽地探究了一些公理之间的逻辑关系，并提出了公理独立性的概念。但实际上，Hilbert在建立他的公理系统时并没有真正遵守他的公理独立性的要求。例如第二类次序公理HII必须依赖第一类关联公理HI进行表达，而第三类全合公理HIII又必须依赖第一类与第二类的公理才能表达。在1899年《几何基础》第一版中罗列的那些公理并不是完全独立的，有些公理就可以从其他公理推导出来。只是在以后的几版中，Hilbert对他的公理系统作了某些修改后，才使得这种“多余”的公理不再出现。为此使某些公理显得很不自然，而且某些直观上极为显然的自明之理也必须从公理推导出来，而这些推导往往是颇为繁琐冗长的。我们认为，仅仅为了减少几个公理而过分追求公理的独立性以致牺牲整个理论的简明性的做法是得不偿失的，是不足取的。对于本书的主题，几何学的机械化说来，更不能对公理之间的独立与否拘泥太甚。　　与公理化的思想相反，Hilbett的原著实质上已蕴含了与本书主题相符的几何学机械化的思想与方法。这一点似乎还从来没有人明确地指出过，甚至Hilbert本人对此是否有明确的认识也很难说。本章以及第2，3章中，我们将说明Hilbert一书在几何学机械化方面所起的巨大作用。　　……

用户评论 (总计3条)

•   这是中国计算机证明数学定理的开山之作，值得读一读。
•   硬面包装，内容很深刻，就是要珍藏、来回翻阅的好书
•   兴趣所致，非专业看看到底说什么？