科技视界
科技視界
과기시계
Science&Technology Vision
2015年
9期
9-11
,共3页
语义Tableau%定理证明器%Prolog
語義Tableau%定理證明器%Prolog
어의Tableau%정리증명기%Prolog
语义Tableau是一种具有较强通用性和适用性的推理方法.基于Prolog语言,并利用语义Tableau方法,在M.C.Fitting提出的一阶逻辑自动定理证明器的基础上提出了一些改进,给出了改进后相应的算法,并且对算法的可终止性和正确性进行了证明.实验结果表明,优化后的语义Tableau定理证明器,大大提高推理效率.
語義Tableau是一種具有較彊通用性和適用性的推理方法.基于Prolog語言,併利用語義Tableau方法,在M.C.Fitting提齣的一階邏輯自動定理證明器的基礎上提齣瞭一些改進,給齣瞭改進後相應的算法,併且對算法的可終止性和正確性進行瞭證明.實驗結果錶明,優化後的語義Tableau定理證明器,大大提高推理效率.
어의Tableau시일충구유교강통용성화괄용성적추리방법.기우Prolog어언,병이용어의Tableau방법,재M.C.Fitting제출적일계라집자동정리증명기적기출상제출료일사개진,급출료개진후상응적산법,병차대산법적가종지성화정학성진행료증명.실험결과표명,우화후적어의Tableau정리증명기,대대제고추리효솔.
