共查询到20条相似文献,搜索用时 93 毫秒
1.
构造型几何定理及其机器证明系统 总被引:1,自引:0,他引:1
Hilbert 机械化定理表明,Pascal 几何中构造型交点定理可以机器证明。1982年,吴文俊教授给出了机械化定理的构造性证法。本文指出,通过添加若干新的构造类型,有更广泛的一类平面几何定理,其机器证明可以按照同样的构造性证法实现,我们称这类定理为构造型几何定理。作者适当调整吴文俊算法的步骤,在 HP1000小型计算机上建立了构造型几何定理的机器证明系统,效率大大提高,从而成功地证明了许多不平凡的几何定理,并且独立发现了相当深入的结果。 相似文献
2.
1986年,洪加威教授发展吴文俊机器证明理论,提出了一类平面几何定理的例证法,这一方法依赖于 Ritt-吴整序原理和吴文俊教授关于升组不可约分解的构造性理论.我们发现例证法适用于证明所有等式型几何定理,即吴几何中的定理.本文应用吴和洪的方法叙述等式型几何定理的例证法,并考虑代数簇的包含关系.目前的讨论仅停留在理论上,这种方法能否用来证明非平凡的几何定理还有待于进一步研究和尝试. 相似文献
3.
几何定理机器证明三十年 总被引:4,自引:1,他引:3
由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今30年,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值方法均能有效地判定其真假,面积法(消点法)、搜索法更能生成其可读的证明.几何不等式机器证明的研究,由于多项式完全判别系统的建立,也有了突破.研究领域已由机器证明扩展为包括几何作图在内的一般几何问题的机器求解,并有了实际的应用. 相似文献
4.
5.
张家驹 《数学的实践与认识》1991,(3)
本文以三个例子——Feuerbach 定理、Pappus 线图象、Simson 定理的机器证明为例说明计算机代数软件 REDUCE 对几何定理的机械化证明的应用. 相似文献
6.
介绍了几何定理机器证明中的“例证法”思想,并挖掘了高等数学中几个“例证法”实例,目的在于建议教师在教学过程中要善于发现并向学生输送新的思想方法,以提高教学质量. 相似文献
7.
计算机的出现,为数学研究提供了强有力的手段,并激起了机械化与构造化的新浪潮.60年代后期开始,计算机代数异军突起,受到人们广泛关注.其中,吴文俊教授1978年在研究几何定理机器证明的过程中,提出了 Wu-Ritt 整序原理,并以此成功的解决了相当一大类几何定理的机器证明.不仅如此,随后的进一步研究工作表明,Wu-Ritt 原 相似文献
8.
9.
10.
11.
12.
13.
在几何定理的机器证明中,遇到可约的情形就会出现重大困难。本文依据代数几何中代数簇相对可约与绝对可约的概念,引进直线与园的定向座标,以避免或至少减轻可约性的困难。作为应用实例,我们对割线定理、Feuerbah 定理以及 Thebault-Taglor-Chou 定理进行了分析,并对最后一个定理给出了比已知要简单得多的机器证明。 相似文献
14.
15.
本文结合吴方法及平面几何的Cliford代数表示,提出了几何定理机器证明的一种完备的方法.用这种方法证明定理时,三角化的过程及证明的过程通常较以前的方法更简短而且它们是可以几何解释的. 相似文献
16.
机器证明的回顾与展望张景中(中国科学院成都计算机应用研究所)机器证明及其应用,是我国攀登计划项目之一.项目核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用.实际上,机器证明研究领域的范围要广泛得多.在国外更一般地叫做自动推理.我们把几... 相似文献
17.
本文结合是吴方法及平面几何的Clifford代数表示,提出了几何定理机器证明的一种完备的方法,用这种方法证明定理时,三角化的过程及证明的过程通常较以前的方法更简短而且它们是可以几何解释的。 相似文献
18.
可持续发展的几何自动推理平台(SGARP)支持用户发展多种多样基于规则的机器自动推理或人机交互推理方法,但缺乏处理符号计算的模块,其解题能力仍有待加强.质点法是最近发展的继面积法之后又一个能对可构造型几何命题生成可读机器证明的具有完全性的算法.基于一种在SGARP中快捷实现符号计算功能的方法,对质点法机器证明算法进行了新的实现.新添加的质点法模块使得用户能更便捷地验证更多的几何定理,从而使SGARP能更好地满足用户学习与发展几何机器推理的需求. 相似文献
19.
1974年,Neal根据Kac和Siegert的思想,给出了一个在电子工程、海洋工程、建筑工程、航空工程、自动控制的随机振动中有重要应用的二阶Volterra非线性系统对平稳正态输入的统计响应的表示定理.1984年,Naess对此定理又给出了一个数学证明.经过研究后发现,他们对定理条件的叙述都是模糊的,而且其数学证明都是有问题的.本文重新讨论了这个表示定理,给出了明确的定理条件及严格的数学证明,为它的广泛应用奠定了理论基础. 相似文献
20.
勾股定理是直角三角形的一个重要性质 ,这个定理被发现至今已有五千多年历史了 .在我国公元前一百多年就记载了勾股定理的应用 .在欧洲通常被称为毕达哥拉斯定理 ,传说毕达哥拉斯为首的学派首先在理论上证明了勾股定理 .据说为庆贺定理的证明 ,他们杀了 10 0头牛祭神 .由此可见 ,勾股定理在人们心目中是何等重要 .勾股定理被发现后 ,它象一块磁石般吸引着世界上许多大人物 ,他们象赶时髦一样参加到证明勾股定理的队伍中来 ,大数学家 ,大物理学家 ,甚至大政治家都来凑热闹 ,都希望在勾股定理的证明中露一下身手 .据说勾股定理的证明方法有 37… 相似文献