The Tableaux based on “unfolding gradually” may produce a lot of repetitive intermediate concept descriptions in deciding the satisfiabilities of acyclic concepts in a variety of description logics, which wastes large space. To tackle this problem, a novel Complete Disjunctive Normal Form (CDNF) algorithm was presented to check the satisfiabilities of acyclic ALCN-concepts. CDNF algorithm built disjunctive normal forms connected by roles in different levels directly on input concept description, and reorganized the input concept description into some hierarchical complete disjunctive normal forms whose satisfiabilities are already known, thus “worked out” satisfiabilities in a real sense. CDNF algorithm employed “one-step” unfolding pattern and acts directly on input concept description, thus eliminated description overlaps to the largest extent. As a result, CDNF algorithm had better performance than tableaux by saving spatial cost linearly or even exponentially.
