计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2014年
8期
1809-1819
,共11页
葛强%张景中%陈矛%彭翕成
葛彊%張景中%陳矛%彭翕成
갈강%장경중%진모%팽흡성
机器证明%可读证明%前推法%向量%回路
機器證明%可讀證明%前推法%嚮量%迴路
궤기증명%가독증명%전추법%향량%회로
machine prove%readable proof%forward chaining%vector%vector loop
几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题目能快速作图,并依据题目类型的不同,分别用不同的向量方法对其进行自动推理,证明结果简短可读.经过大量实例测试,证明将向量用于几何自动推理是可行和高效的.与《超级画板》等中的证明器相比,文中算法在自动推理能力和证明过程可读性方面有较大提高.文中给出的基于向量的几何可读证明算法丰富了几何定理自动推理方法,并且具有应用于几何教学实践的价值.
幾何定理機器證明已經成功髮展瞭多種新方法,但其中對中學幾何中嚮量的機器證明研究沒有抓住其迴路的基本特徵.文中以嚮量的迴路為齣髮點,提齣瞭基于迴路的嚮量可讀證明新方法,開髮瞭機器證明新程序.該程序對常見的構造類型歐氏幾何題目能快速作圖,併依據題目類型的不同,分彆用不同的嚮量方法對其進行自動推理,證明結果簡短可讀.經過大量實例測試,證明將嚮量用于幾何自動推理是可行和高效的.與《超級畫闆》等中的證明器相比,文中算法在自動推理能力和證明過程可讀性方麵有較大提高.文中給齣的基于嚮量的幾何可讀證明算法豐富瞭幾何定理自動推理方法,併且具有應用于幾何教學實踐的價值.
궤하정리궤기증명이경성공발전료다충신방법,단기중대중학궤하중향량적궤기증명연구몰유조주기회로적기본특정.문중이향량적회로위출발점,제출료기우회로적향량가독증명신방법,개발료궤기증명신정서.해정서대상견적구조류형구씨궤하제목능쾌속작도,병의거제목류형적불동,분별용불동적향량방법대기진행자동추리,증명결과간단가독.경과대량실례측시,증명장향량용우궤하자동추리시가행화고효적.여《초급화판》등중적증명기상비,문중산법재자동추리능력화증명과정가독성방면유교대제고.문중급출적기우향량적궤하가독증명산법봉부료궤하정리자동추리방법,병차구유응용우궤하교학실천적개치.
