Abstract
The task of pinpointing the relevant subsets of axioms for a given property has acquired relevancy in the last years. In this paper we show how automata-based decision procedures can be adapted to produce a so-called pinpointing formula. The relevance of this method is method is shown by giving an (optimal) algorithm that computes pinpointing formulas for unsatisfiability of SI concepts w.r.t. general TBoxes.