New reasoning algorithm based on EFALC

摘要

The current extended fuzzy description logics lack reasoning algorithms with TBoxes. The problem of the satisfiability of the extended fuzzy description logic EFALC cut concepts w. r. t. TBoxes is proposed, and a reasoning algorithm is given. This algorithm is designed in the style of tableau algorithms, which is usually used in classical description logics. The transformation rules and the process of this algorithm is described and optimized with three main techniques: recursive procedure call, branch cutting and introducing sets of mesne results. The optimized algorithm is proved sound, complete and with an EXPTime complexity, and the satisfiability problem is EXPTime-complete.