计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2010年
7期
126-129
,共4页
李涛%张波%章潜才%鹿海涛%巫莉莉
李濤%張波%章潛纔%鹿海濤%巫莉莉
리도%장파%장잠재%록해도%무리리
自动推理%可读证明%表达式%谓词
自動推理%可讀證明%錶達式%謂詞
자동추리%가독증명%표체식%위사
计算机自动推理和几何定理机器证明已经取得令人瞩目的成果,自动推理的软件也出现了很多.完善解决表达式的推理是数学定理机械化证明必须达到的目的,但是关于表达式的推理还缺乏研究,因为表达式的推理不同于一般信息的推理,它没有固定的格式,信息表述复杂.本文在之前研究工作的基础上,通过对表达式在推理时的特征分析,提出一种表达式推理的方法,是向这个方向的一个尝试.在该方法中,通过适当的替换,将表达式化为空,从而实现了表达式的简单处理,并在文中列举几个实例进行分析.实践证明,利用这种方法,可对大多数的结论为表达式的几何命题给出可读证明过程.
計算機自動推理和幾何定理機器證明已經取得令人矚目的成果,自動推理的軟件也齣現瞭很多.完善解決錶達式的推理是數學定理機械化證明必鬚達到的目的,但是關于錶達式的推理還缺乏研究,因為錶達式的推理不同于一般信息的推理,它沒有固定的格式,信息錶述複雜.本文在之前研究工作的基礎上,通過對錶達式在推理時的特徵分析,提齣一種錶達式推理的方法,是嚮這箇方嚮的一箇嘗試.在該方法中,通過適噹的替換,將錶達式化為空,從而實現瞭錶達式的簡單處理,併在文中列舉幾箇實例進行分析.實踐證明,利用這種方法,可對大多數的結論為錶達式的幾何命題給齣可讀證明過程.
계산궤자동추리화궤하정리궤기증명이경취득령인촉목적성과,자동추리적연건야출현료흔다.완선해결표체식적추리시수학정리궤계화증명필수체도적목적,단시관우표체식적추리환결핍연구,인위표체식적추리불동우일반신식적추리,타몰유고정적격식,신식표술복잡.본문재지전연구공작적기출상,통과대표체식재추리시적특정분석,제출일충표체식추리적방법,시향저개방향적일개상시.재해방법중,통과괄당적체환,장표체식화위공,종이실현료표체식적간단처리,병재문중열거궤개실례진행분석.실천증명,이용저충방법,가대대다수적결론위표체식적궤하명제급출가독증명과정.
