A Tableaux Decision Procedure for Fuzzy Description Logic FALNUI

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 trnslated 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 FALNUI tableaux reasoning algorithms.