软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2010年
8期
1863-1877
,共15页
古华茂%王勋%凌云%高济
古華茂%王勛%凌雲%高濟
고화무%왕훈%릉운%고제
描述逻辑推理%可满足性%析取范式%SHOIN(D)%Tableau
描述邏輯推理%可滿足性%析取範式%SHOIN(D)%Tableau
묘술라집추리%가만족성%석취범식%SHOIN(D)%Tableau
针对非循环概念提出了一种对SHOIN(D)-概念可满足性进行判断的方法--CDNF(complete disjunctive normal form)算法.该算法通过把非循环定义的概念描述本身构建成分层次的析取范式群,并通过子句重用技术阻止无谓的子概念扩展,这样的析取范式群具有可满足性自明性,从而可以实现对SHOIN(D)-概念可满足性的直接判断.该算法基本上消除了判断过程中描述重复的现象,从而在空间、时间性能上都比Tableau算法有更好的表现.
針對非循環概唸提齣瞭一種對SHOIN(D)-概唸可滿足性進行判斷的方法--CDNF(complete disjunctive normal form)算法.該算法通過把非循環定義的概唸描述本身構建成分層次的析取範式群,併通過子句重用技術阻止無謂的子概唸擴展,這樣的析取範式群具有可滿足性自明性,從而可以實現對SHOIN(D)-概唸可滿足性的直接判斷.該算法基本上消除瞭判斷過程中描述重複的現象,從而在空間、時間性能上都比Tableau算法有更好的錶現.
침대비순배개념제출료일충대SHOIN(D)-개념가만족성진행판단적방법--CDNF(complete disjunctive normal form)산법.해산법통과파비순배정의적개념묘술본신구건성분층차적석취범식군,병통과자구중용기술조지무위적자개념확전,저양적석취범식군구유가만족성자명성,종이가이실현대SHOIN(D)-개념가만족성적직접판단.해산법기본상소제료판단과정중묘술중복적현상,종이재공간、시간성능상도비Tableau산법유경호적표현.
