查看几何定理机器证明的源代码
←
几何定理机器证明
跳转至:
导航
、
搜索
因为以下原因,你没有权限编辑本页:
你刚才请求的操作只对属于该用户组的用户开放:
用户
您可以查看并复制此页面的源代码:
'''几何定理机器证明'''([[英语]]:mechanical theorem-proving in geometry),用[[计算机]]自动证明某一类型几何定理,甚至某一种几何全部定理的原理和方法。从理论角度看,几何定理的机器证明要经历公理化、代数化与坐标化、机械化等步骤,才能编制程序并在计算机上实现。可用机器证明的几何定理(主要是初等几何的定理)有三种不同类型,与之对应则有三种不同的机器证明方法。每一类型定理的机器证明都必须假设代数化与坐标化已经完成,而且可把几何定理的证明问题化为一些代数关系式的处理问题。①第一类型定理的特征是假设部分的所有代数关系式对于某些特定变量都必须是线性的,包括一类构造型的纯交点定理,其对应的机器证明方法称为希尔伯特方法;②第二类型定理的特征是假设和终结部分的代数关系式都可用多项式的方程来表示,其对应的机器证明方法是中国数学家吴文俊首先提出的,称为吴文俊方法;③第三类型定理的特征是假设和终结部分可以是任意的多项式等式或不等式,但其系数必须在一实闭域中,因而原来的几何必须有次序关系,其对应的机器证明方法称为塔斯基方法。这三种方法各有其适用范围,但就可以通用的那些定理证明问题来说,希尔伯特法效率最高而塔斯基法效率最低,但是前者的适用范围很窄。1980年在 HP9835A机上,用吴文俊方法成功地证明了勾股定理、西姆逊线定理、帕普斯定理、帕斯卡定理、费尔巴哈定理,并在45个帕斯卡点中发现了20条帕斯卡圆锥曲线,这种方法还推广到微分几何,将微分几何曲线论中的贝屈朗定理推广到仿射微分几何。吴文俊的研究成果引起了国际学术界的重视。 ===参见=== *[[人工智能基本条目]] *[[计算机科学技术基本条目]] *[[工学(目录)]] * [[人工智能]] * [[计算机科学]] * [[机器人学]] * [[语言列表]] * [[人工语言]] ** [[形式语言]] * [[知识表示]] [[Category:工学]] [[Category:计算机科学与技术]] [[Category:人工智能| ]] [[Category:控制论]] [[Category:形式科学]] [[Category:技术与社会]] [[Category:计算神经科学]] [[Category:新兴技术]] [[Category:知识管理]] [[Category:信息科学]] [[Category:语言]] [[Category:语言学]] [[Category:自然语言处理]] [[Category:计算语言学]] [[Category:自动控制]] [[Category:系统工程]] [[Category:中文词典]] [[Category:J音词条]] [[Category:几]]
返回
几何定理机器证明
。
导航菜单
个人工具
创建账户
登录
名字空间
页面
讨论
变种
查看
阅读
查看源代码
查看历史
操作
搜索
导航
首页
最近更改
随机页面
工具箱
链入页面
相关更改
特殊页面
页面信息
扫描二维码可以用手机浏览词条