Deciding Fuzzy Description Logics by Type Elimination?

Abstract. We present a novel procedure FixIt(ALC) for deciding knowledge base satisfiability in the Fuzzy Description Logic (FDL) ALC. FixIt(ALC) does not search for tree-structured models as in tableau-based proof procedures, but embodies a fixpoint-computation of canonical models that are not necessar-ily tree-structured. Conceptually, the procedure is based on a type-elimination process. Soundness, completeness and termination are proven. To the best of our knowledge it is the first fixpoint-based decision procedure for FDLs, hence intro-ducing a new class of inference procedures into FDL reasoning.