Model contractions on description logics

Abstract

When using tableaux algorithms to reason about Description Logics (DLs), new information is inferred from the models considered while trying to achieve knowledge satisfiability. By focusing the ontology change problem, we consider an environment where DLs are the logical formalization to express knowledge bases in the web, and the integration of distributed ontologies is developed under new extensions of the belief revision theories originally exposed in [1]. Hence, a reinforced theory arises in order to properly apply change operations over models, considering new inferred information and assumed beliefs in each possible world. As a result, a new type of contraction operator is proposed and its success postulate analyzed.