Because widely used real-world ontologies are often complex and large, one important challenge has emerged: designing tools for users to focus on sub-ontologies corresponding to their specific interests. To this end, various modules have been introduced to provide concise ontology views. This work concentrates on extracting deductive modules that preserve logical entailment over a given vocabulary. Existing deductive module proposals are either inefficient from a computing point of view or unsatisfactory from a quality point of view because the modules extracted are not concise enough. For example, minimal modules guarantee the most concise results, but their computation is highly time-consuming, while ⊥⊤∗-modules are easy to compute but usually contain many redundant items. To overcome computation cost and lack of quality, we propose to compute two kinds of deductive modules called pseudo-minimal modules and complete modules for EL-ontology. Our deductive module definitions rely on associating a tree representation with an ontology, and their computation is based on SAT encoding. Our experiments on real-world ontologies show that our pseudo-minimal modules are indeed minimal modules in almost all cases (98.9%), and computing pseudo-minimal modules is more efficient (99.79 times faster on average) than the state-of-the-art method Zoom for computing minimal modules. Also, our complete modules are more compact than ⊥⊤∗-modules, but their computation time remains comparable. Finally, note that our proposal applies to EL-ontologies while Zoom only works for EL-terminologies.

We present a method for extracting general modules for ontologies formulated in the description logic ALC. A module for an ontology is an ideally substantially smaller ontology that preserves all entailments for a user-specified set of terms. As such, it has applications such as ontology reuse and ontology analysis. Different from classical modules, general modules may use axioms not explicitly present in the input ontology, which allows for additional conciseness. So far, general modules have only been investigated for lightweight description logics. We present the first work that considers the more expressive description logic ALC. In particular, our contribution is a new method based on uniform interpolation supported by some new theoretical results. Our evaluation indicates that our general modules are often smaller than classical modules and uniform interpolants computed by the state-of-the-art, and compared with uniform interpolants, can be computed in significantly shorter time. Moreover, our method can be used for, and in fact, improves the computation of uniform interpolants and classical modules.

For knowledge intensive domains, such as Avionics Maintenance, applying automated analysis comes with a major challenge: formalizing complex domain knowledge and conceiving suitable automated algorithms for real world requirements. In this paper, we propose a study on knowledge discovery to assist avionics maintenance via identifying meaningful Description Logic based complex concepts, called situation discovery, that corresponds to crucial scenarios during device repair. We propose an approach to automatic learning of relevant situations hidden in an ontology, in an unsupervised way. Distinct from ontology based concept learning, where a set of instances is given as positive examples of a target concept, the challenge of learning hidden situations consists in discovering significant situations from exponentially many unknown situations. In this paper we formalize the problem and study some related complexity results as well as the algorithms to solve the problem, together with its application to Avionics Maintenance. The approach has been integrated into an enterprise system and achieves the state-of-the-art result in this application.

Ontologies can represent knowledge in a structured and formally well-understood way, which is crucial for information sharing. However, in practice, it is often difficult to have an error-free ontology. Conflicts can occur due to modeling errors or ontology merging and evolution. Moreover, uncertainty can happen because of modeling choices or the lack of confidence for a constructed ontology. Argumentation frameworks for knowledge bases reasoning and management have received extensive interests in the field of Artificial Intelligence in recent years. In this paper, we propose a unified framework to handle conflicts in uncertain ontologies with the use of deductive argumentation. Different from existing approaches, we introduce a stronger notion of conflict that covers both inconsistency and incoherence, where the latter is a special contradiction that can occur in an ontology. The unified approach spreads uncertainty degrees throughout argumentation trees and the enriched argument structure leads us to two novel inference relations. We then present a method to compute (counter)-arguments as well as argumentation trees in the context of uncertain ontologies based on the developments of three notions called minimal conflicting subontologies, maximal nonconflicting subontologies, and prudent justifications.

International audience

In the presence of an ever growing amount of information, organizations and human users need to be able to focus on certain key pieces of information and to intentionally ignore all other possibly relevant parts. Knowledge about complex systems that is represented in ontologies yields collections of axioms that are too large for human users to browse, let alone to comprehend or reason about it. We introduce the notion of an ontology excerpt as being a fixed-size subset of an ontology, consisting of the most relevant axioms for a given set of terms. These axioms preserve as much as possible the knowledge about the considered terms described in the ontology. We consider different extraction techniques for ontology excerpts based on methods from the area of information retrieval. To evaluate these techniques, we propose to measure the degree of incompleteness of the resulting excerpts using the notion of logical difference.

DL-Lite is an important family of description logics. Recently, there is an increasing interest in handling inconsistency in DL-Lite as the constraint imposed by a TBox can be easily violated by assertions in ABox in DL-Lite. In this paper, we present a distance-based paraconsistent semantics based on the notion of feature in DL-Lite, which provides a novel way to rationally draw meaningful conclusions even from an inconsistent knowledge base. Finally, we investigate several important logical properties of this entailment relation based on the new semantics and show its promising advantages in non-monotonic reasoning for DL-Lite.

Measuring inconsistency is recognized as an important issue for handling inconsistencies [5, 6]. Based on prime implicates canonical representation, we first characterize the conflicting variables allowing us to refine an existing inconsistency measure. Secondly, we propose a new measure, to circumscribe the internal conflicts in a knowledge base. This measure is proved to satisfy a new but weaker form of dominance.

Measuring inconsistency is recognized as an important issue for handling inconsistencies. Good measures are supposed to satisfy a set of rational properties. However, defining sound properties is sometimes problematic. In this paper, we emphasize one such property, named dominance, rarely satisfied by syntactic measures. Based on prime implicates canonical representation, we first characterize the conflicting variables allowing us to refine an existing inconsistency measure. Secondly, we propose a new measure, to circumscribe the internal conflicts in a knowledge base. This measure is proved to satisfy a new but weaker form of dominance.

There exist a handful of natural language processing and machine learning approaches for extracting Description Logic concept definitions from natural language texts. Typically, for a single target concept several textual sentences are used, from which candidate concept descriptions are obtained. These candidate descriptions may have confidence values associated with them. In a final step, the candidates need to be combined into a single concept, in the easiest case by selecting a relevant subset and taking its conjunction. However, concept descriptions generated in this manner can contain false information, which is harmful when added to a formal knowledge base. In this paper, we claim that this can be improved by considering formal constraints that the target concept needs to satisfy. We first formalize a reasoning problem for the selection of relevant candidates and examine its computational complexity. Then, we show how it can be reduced to SAT, yielding a practical algorithm for its solution. Furthermore, we describe two ways to construct formal constraints, one is automatic and the other interactive. Applying this approach to the SNOMED CT ontology construction scenario, we show that the proposed framework brings a visible benefit for SNOMED CT development.

Consistent query answering over description logic based ontologies is an important topic in ontology engineering as it can provide meaningful answers to queries posed over inconsistent ontologies. Current approaches for dealing with this problem usua

Measuring inconsistency in knowledge bases has been recognized as an important problem in several research areas. Many methods have been proposed to solve this problem and a main class of them is based on some kind of paraconsistent semantics. However, existing methods suffer from two limitations: (i) they are mostly restricted to propositional knowledge bases; (ii) very few of them discuss computational aspects of computing inconsistency measures. In this article, we try to solve these two limitations by exploring algorithms for computing an inconsistency measure of first-order knowledge bases. After introducing a four-valued semantics for first-order logic, we define an inconsistency measure of a first-order knowledge base, which is a sequence of inconsistency degrees. We then propose a precise algorithm to compute our inconsistency measure. We show that this algorithm reduces the computation of the inconsistency measure to classical satisfiability checking. This is done by introducing a new semantics, named S[n]-4 semantics, which can be calculated by invoking a classical SAT solver. Moreover, we show that this auxiliary semantics also gives a direct way to compute upper and lower bounds of inconsistency degrees. That is, it can be easily revised to compute approximating inconsistency measures. The approximating inconsistency measures converge to the precise values if enough resources are available. Finally, by some nice properties of the S[n]-4 semantics, we show that some upper and lower bounds can be computed in P-time, which says that the problem of computing these approximating inconsistency measures is tractable.

Measuring Inconsistency in ontologies is an important topic in ontology engineering as it can provide extra information for dealing with inconsistency. Many approaches have been proposed to deal with this issue. However, the main drawback of these algorithms is their high computational complexity. One of the main sources of the high complexity is the intractability of the underlying Description Logics (DLs). In this paper, we focus on an important tractable DL family, \emph{DL-Lite}. We define an inconsistency degree of a \emph{DL-Lite} ontology based on a three-valued semantics. We also present an algorithm to compute this inconsistency degree and show that its time-complexity is PTime in the size of ABox and TBox.