论文部分内容阅读
自动推理是人工智能领域的重要研究课题.Horn子句作为一种特殊的子句有着很好形式和良好的性质，在逻辑推理方面基于Horn子句上的归结往往显得简单而快速.又比如OI消解对一般子句是不完备的，但是对于Horn子句它是完备的.文章在命题逻辑中给出了将一般子句转化成Horn子句的条件与方法.并用同态的方法证明了转化前后两个子句集的可满足性(不可满足性)的一致性.