计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2014年
6期
1341-1351
,共11页
张景中%张传军%郑焕%饶永生%邹宇
張景中%張傳軍%鄭煥%饒永生%鄒宇
장경중%장전군%정환%요영생%추우
可由用户持续发展的几何自动推理平台(SGARP)%几何定理机器证明%符号计算%Python语言%质点法%Thebault定理
可由用戶持續髮展的幾何自動推理平檯(SGARP)%幾何定理機器證明%符號計算%Python語言%質點法%Thebault定理
가유용호지속발전적궤하자동추리평태(SGARP)%궤하정리궤기증명%부호계산%Python어언%질점법%Thebault정리
sustainable%geometry%automated%reasoning%platform%(SGARP)%automated%geometry%theorem%proving%symbolic%computation%Python%language%mass%point%method%Thebault's%theorem
可持续发展的几何自动推理平台(sustainable geometry automated reasoning platform,SGARP)支持用户按需添加或修改几何定理机器证明所涉及的几何对象、谓词、定理和规则,以发展多种多样基于规则的机器自动推理或人机交互推理方法.为进一步提高SGARP的推理能力和扩展其适用范围,提出一种在SGARP中实现符号计算功能的快捷方法,并成功添加了质点法和解析法推理模块.质点法可证明希尔伯特交点类几何命题,解析法能用于辅助证明各种类型有一定难度的几何定理,如著名的Thebault定理.对这两种方法用基于Web的机器证明测试用的几何问题库(thousands of geometric problems for geometric theorem provers,TGTP)中180道几何题进行评估,均在合理时间内给出令人满意的可读机器证明,表明升级后的SGARP能更好地满足用户学习与发展几何机器推理的需求.
可持續髮展的幾何自動推理平檯(sustainable geometry automated reasoning platform,SGARP)支持用戶按需添加或脩改幾何定理機器證明所涉及的幾何對象、謂詞、定理和規則,以髮展多種多樣基于規則的機器自動推理或人機交互推理方法.為進一步提高SGARP的推理能力和擴展其適用範圍,提齣一種在SGARP中實現符號計算功能的快捷方法,併成功添加瞭質點法和解析法推理模塊.質點法可證明希爾伯特交點類幾何命題,解析法能用于輔助證明各種類型有一定難度的幾何定理,如著名的Thebault定理.對這兩種方法用基于Web的機器證明測試用的幾何問題庫(thousands of geometric problems for geometric theorem provers,TGTP)中180道幾何題進行評估,均在閤理時間內給齣令人滿意的可讀機器證明,錶明升級後的SGARP能更好地滿足用戶學習與髮展幾何機器推理的需求.
가지속발전적궤하자동추리평태(sustainable geometry automated reasoning platform,SGARP)지지용호안수첨가혹수개궤하정리궤기증명소섭급적궤하대상、위사、정리화규칙,이발전다충다양기우규칙적궤기자동추리혹인궤교호추리방법.위진일보제고SGARP적추리능력화확전기괄용범위,제출일충재SGARP중실현부호계산공능적쾌첩방법,병성공첨가료질점법화해석법추리모괴.질점법가증명희이백특교점류궤하명제,해석법능용우보조증명각충류형유일정난도적궤하정리,여저명적Thebault정리.대저량충방법용기우Web적궤기증명측시용적궤하문제고(thousands of geometric problems for geometric theorem provers,TGTP)중180도궤하제진행평고,균재합리시간내급출령인만의적가독궤기증명,표명승급후적SGARP능경호지만족용호학습여발전궤하궤기추리적수구.
