论文部分内容阅读
传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[1]中,给出了一个实用而紧致的知识的语义模型——知识结构(knowledge struc- ture),并给出相应的利用BDD(Binary Decision Diagram)的符号化计算方法,实验表明这种基于BDD的算法比传统方法有很大的优势,但这种基于BDD的方法在计算规模大的例子时仍存在明显的组合爆炸。文章在知识结构(knowledge structure)的语义基础上,通过挖掘知识结构语义中各元素的关系,把知识的计算规约于可满足性问题(SAT),因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD。实验结果证实了这种方法的有效性。
The traditional knowledge reasoning algorithm mainly relies on the universal theorem prover, so there will be obvious combinatorial explosion problems and semi-automation problems, which can only deal with small-scale problems. In [1], a practical and compact semantic model of knowledge is given, and a corresponding symbolic computation method using BDD (Binary Decision Diagram) is given. Experiments It shows that this BDD-based algorithm has a great advantage over the traditional methods. However, this BDD-based method still has obvious combination explosion in calculating large-scale examples. Based on the semantics of the knowledge structure, the article defines the calculation of knowledge on the Satisfiability Problem (SAT) by mining the relationships among the elements in the semantic of the knowledge structure. Because SAT Solver uses the symbolic computation and computational scale And efficiency should be significantly better than BDD. The experimental results confirm the validity of this method.