计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2009年
11期
3064-3067
,共4页
一阶逻辑%自动证明%可满足性%子句搜索方法%部分实例化方法
一階邏輯%自動證明%可滿足性%子句搜索方法%部分實例化方法
일계라집%자동증명%가만족성%자구수색방법%부분실례화방법
first-order logic%automated reasoning%satisfiability%clause searching method%partial instantiation method
子句集的可满足性判定是自动证明领域的热点之一.提出了子句搜索方法判定命题子句集Φ的可满足性,该方法查找Φ中子句的一个公共不可扩展子句C,当且仅当找到C时Φ可满足,此时C中各文字的补构成一个模型.结合部分实例化方法将子句搜索方法提升至一阶.一阶子句搜索方法可以判定子句集的M可满足性,具备终止性、正确性和完备性,是一种判定子句集可满足性的有效方法.
子句集的可滿足性判定是自動證明領域的熱點之一.提齣瞭子句搜索方法判定命題子句集Φ的可滿足性,該方法查找Φ中子句的一箇公共不可擴展子句C,噹且僅噹找到C時Φ可滿足,此時C中各文字的補構成一箇模型.結閤部分實例化方法將子句搜索方法提升至一階.一階子句搜索方法可以判定子句集的M可滿足性,具備終止性、正確性和完備性,是一種判定子句集可滿足性的有效方法.
자구집적가만족성판정시자동증명영역적열점지일.제출료자구수색방법판정명제자구집Φ적가만족성,해방법사조Φ중자구적일개공공불가확전자구C,당차부당조도C시Φ가만족,차시C중각문자적보구성일개모형.결합부분실례화방법장자구수색방법제승지일계.일계자구수색방법가이판정자구집적M가만족성,구비종지성、정학성화완비성,시일충판정자구집가만족성적유효방법.
Deciding satisfiability of clause set is one of the active research topics in the automated reasoning field. A clause searching method of deciding satisfiability of prepositional clause set Φ was proposed. This method first searched one clause C which cannot be extended from all clauses in Φ, if and only if C exists Φ was satisfied and the negative of C was one model. The authors updated clause searching method to first-order by partial instantiation method. Clause searching method in first-order logic can decide M satisfiability of clause set and is of terminating, sound and complete property. It is a valid method for deciding satisfiability of clause set.
