Abstract
Fuzzy description logics (DLs) serve as a tool to handle vagueness in real-world knowledge. There is particular interest in logics implementing ?ukasiewicz semantics, which has a number of favourable properties. Current decision procedures for ?ukasiewicz fuzzy DLs work by reduction to exponentially large mixed integer programming problems. Here, we present a decision method that stays closer to logical syntax, a labelled tableau algorithm for ?ukasiewicz Fuzzy ALC that calls only on (pure) linear programming, and this only to decide atomic clashes. The algorithm realizes the best known complexity bound, NEXPTIME. Our language features a novel style of fuzzy ABoxes that work with comparisons of truth degrees rather than explicit numerical bounds.