re-Horn子句集的Horn化及可满足性判定方法  

Transforming re-horn sets into horn sets and satisfiability determination

作　　者：安世勇 徐扬[2] 

机构地区：[1]西南交通大学数学学院,四川成都610031 [2]西南交通大学智能开发中心,四川成都610031

出　　处：《济南大学学报（自然科学版）》2015年第5期346-349,共4页Journal of University of Jinan(Science and Technology)

基　　金：国家自然科学基金(61175055)

摘　　要：在命题逻辑中给出将re-Horn子句转化成Horn子句的条件与方法,用同态的方法证明转化前后2个子句集的可满足性或不可满足性的一致性,给出re-Horn子句集的可满足性的判定方法。Firstly the condition and method for transforming a re-Horn clause to a Horn clause are given. Secondly,on the basis of homomorphism,that the transformation will result in a consistent Horn clause in satisfiability or unsatisfiability is proved. Finally the satisfiability determination of a re-Horn set is also studied.

关 键 词：命题逻辑 HORN子句 子句集 可满足性 同态 

分 类 号：O141.12[理学—数学]