基于向量的几何可读自动证明

• 作者: 张景中 彭翕成 葛强 陈矛
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 机器证明 可读证明 前推法 向量 回路
• 年，卷（期）: 2014,（8）
• 所属期刊栏目: 计算机软件与理论
• 页码范围: 1809-1819
• 页数: 11页
• 分类号: TP181
• 字数: 9896字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2014.01809

摘要

几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题目能快速作图,并依据题目类型的不同,分别用不同的向量方法对其进行自动推理,证明结果简短可读.经过大量实例测试,证明将向量用于几何自动推理是可行和高效的.与《超级画板》等中的证明器相比,文中算法在自动推理能力和证明过程可读性方面有较大提高.文中给出的基于向量的几何可读证明算法丰富了几何定理自动推理方法,并且具有应用于几何教学实践的价值.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	彭翕成	华中师范大学国家数字化学习工程技术研究中心	115	337	9.0	17.0
2	张景中	华中师范大学国家数字化学习工程技术研究中心	36	370	11.0	18.0
3	葛强	河南大学数据与知识工程研究所	18	146	7.0	12.0
5	陈矛	华中师范大学国家数字化学习工程技术研究中心	10	103	6.0	10.0