软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2009年
6期
1521-1527
,共7页
李莹%孙吉贵%吴瑕%朱兴军
李瑩%孫吉貴%吳瑕%硃興軍
리형%손길귀%오하%주흥군
定理机器证明%命题逻辑%扩展规则%启发式策略%归结
定理機器證明%命題邏輯%擴展規則%啟髮式策略%歸結
정리궤기증명%명제라집%확전규칙%계발식책략%귀결
基于扩展规则的方法是一种定理证明方法.在IER(improved extension rule)扩展规则算法的基础上,提出了IMOM(improved maximum occurrences on clauses of maximum size)和IBOHM(improved BOHM)启发式策略,并将两种启发式策略用于IER算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法IMOMH IER和IBOHMH_IER.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问题是否可满足,故其速度平均能够达到原有算法DR(directional resolution)和IER的10～200倍.
基于擴展規則的方法是一種定理證明方法.在IER(improved extension rule)擴展規則算法的基礎上,提齣瞭IMOM(improved maximum occurrences on clauses of maximum size)和IBOHM(improved BOHM)啟髮式策略,併將兩種啟髮式策略用于IER算法中,有指導性地選擇限定搜索空間的子句,設計併實現瞭算法IMOMH IER和IBOHMH_IER.實驗結果錶明,由于這兩種啟髮式策略能夠選擇較為閤適的搜索空間,可以儘快地判定齣原問題是否可滿足,故其速度平均能夠達到原有算法DR(directional resolution)和IER的10～200倍.
기우확전규칙적방법시일충정리증명방법.재IER(improved extension rule)확전규칙산법적기출상,제출료IMOM(improved maximum occurrences on clauses of maximum size)화IBOHM(improved BOHM)계발식책략,병장량충계발식책략용우IER산법중,유지도성지선택한정수색공간적자구,설계병실현료산법IMOMH IER화IBOHMH_IER.실험결과표명,유우저량충계발식책략능구선택교위합괄적수색공간,가이진쾌지판정출원문제시부가만족,고기속도평균능구체도원유산법DR(directional resolution)화IER적10～200배.
