re-Horn子句集的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.%在命题逻辑中给出将re-Horn子句转化成Horn子句的条件与方法,用同态的方法证明转化前后2个子句集的可满足性或不可满足性的一致性,给出re-Horn子句集的可满足性的判定方法.