基于无穷Horn子句集的推理编译

摘要

Horn子句在知识表示和知识处理中有广泛的应用,但在一阶谓词逻辑系统内部,许多公式都不能转换为等价的Horn子句形式.本文提出一种称为推理编译的方法,能够将一大类形式逻辑系统(包括一阶谓词逻辑)中的推理问题等价转换为一种特殊命题逻辑——泛阶命题逻辑中子句个数无穷的Horn子句集的推理问题,因此可在命题逻辑的框架内统一处理大多数逻辑的推理问题,并可为这些逻辑系统找到一致的语义解释.