Understanding the complexity of axiom pinpointing in lightweight description logics

Lightweight description logics are knowledge representation formalisms characterised by the low complexity of their standard reasoning tasks. They have been successfully employed for constructing large ontologies that model domain knowledge in several different practical applications. In order to maintain these ontologies, it is often necessary to detect the axioms that cause a given consequence. This task is commonly known as axiom pinpointing. In this paper, we provide a thorough analysis of the complexity of several decision, counting, and enumeration problems associated to axiom pinpointing in lightweight description logics. (C) 2017 Elsevier B.V. All rights reserved.