计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2009年
1期
9-14
,共6页
孙吉贵%李莹%朱兴军%吕帅
孫吉貴%李瑩%硃興軍%呂帥
손길귀%리형%주흥군%려수
定理机器证明%命题逻辑%扩展规则%可满足性问题%归结
定理機器證明%命題邏輯%擴展規則%可滿足性問題%歸結
정리궤기증명%명제라집%확전규칙%가만족성문제%귀결
基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法,首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时问和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.
基于擴展規則的定理證明方法是一種與歸結方法互補的新的定理證明方法,首先通過對擴展規則的深入研究,給齣瞭擴展規則的一箇重要性質,設計併實現瞭該性質的判定算法.此外,從理論上分析及證明瞭該判定算法的時問和空間複雜性.基于此,提齣瞭一種新的基于擴展規則的定理證明算法NER,將判定子句集可滿足性問題轉化為一繫列文字集閤的包含問題,而非計數問題.實驗結果錶明,算法NER的執行效率較原有擴展規則算法IER和基于歸結的有嚮歸結算法DR有明顯提高,有些問題可以提高兩箇數量級.
기우확전규칙적정리증명방법시일충여귀결방법호보적신적정리증명방법,수선통과대확전규칙적심입연구,급출료확전규칙적일개중요성질,설계병실현료해성질적판정산법.차외,종이론상분석급증명료해판정산법적시문화공간복잡성.기우차,제출료일충신적기우확전규칙적정리증명산법NER,장판정자구집가만족성문제전화위일계렬문자집합적포함문제,이비계수문제.실험결과표명,산법NER적집행효솔교원유확전규칙산법IER화기우귀결적유향귀결산법DR유명현제고,유사문제가이제고량개수량급.
