模糊描述逻辑FALNUI的tableaux推理

A Tableaux Decision Procedure for Fuzzy Description Logic FALNUI

分析了模糊描述逻辑FALNUI与模糊ER模型的关系,即模糊ER模型可以转化为FALNUI的知识库,并且模糊ER模型的可满足性、冗余性和包含关系等推理问题可以转化为FALNUI的包含推理问题,但FALNUI缺乏相应的推理算法.提出了一种基于描述逻辑tableaux的FALNUI的可满足性推理算法,证明了该推理算法的正确性,以及提出了FALNUI的Tbox扩展和去除方法,证明了FAL-NUI的包含推理问题可以转化为可满足性推理问题,并给出了FALNUI的包含推理算法.FALNUI的tableaux推理算法为模糊ER模型的可满足性、冗余性和包含关系等自动推理的实现提供了理论基础.

ER model may be translated into description logic ALNUI knowledge bases, and the reasoning on ER model may be reduced to model reasoning on ALNUI knowledge bases. Fuzzy description logic FALNUI is the fuzzy extension of description logic ALNUI through fuzzy logic, and the syntax and semantics of FALNUI are given. The relationship of description logic FALNUI and fuzzy ER model is investigated, i.e., fuzzy ER model may be translated into FALNUI knowledge bases, and reasoning problem of satisfiability, redundancy, and subsumption relation of fuzzy ER model may be translated into FALNUI subsumption reasoning problem, but FALNUI lacks reasoning algorithms for satisfiability and subsumption reasoning tasks at present. A kind of description logic tableaux based satisfiability reasoning algorithm for FALNUI is presented, and the correctness of the satisfiability reasoning algorithm is proved. The Tbox expansion and elimination methods for FALNUI are presented. It is proved that subsumption reasoning problem may be translated into satisfiability reasoning problem in FALNUI too, and subsumption reasoning algorithm for FALNUI is presented through Tbox expansion and elimination. Therefore, the theoretical foundation for the implementation of automatic reasoning of satisfiability, redundancy, and subsumption relation of fuzzy ER model is presented through fuzzy description logic FALNU[ tableaux reasoning algorithms.