We propose an extension of Description Logics (DLs) with generic concepts and conditional axioms. Inspired by object-oriented languages, generic concepts allow a compact definition of concepts with similar structures. For example, one can define a generic concept Owner[X] to describe objects that own another object from X, and later use a specific replacement of the parameter X, such as Owner[Pet] representing pet owners. Conditional axioms can be used to set bounds on the values that replace the generic parameters. For example, we could restrict replacements of X in a concept Keeper[X] to only subconcepts of Pet. As the set of possible parameter replacements can be infinite and even uncountable, the generic extensions are, in general, undecidable. To identify decidable generic DLs, we focus on the case of terminologies, requiring that variables are only used in definitions of generic concepts. We formulate restrictions that allow a reduction of generic entailment to classical entailment and further conditions that ensure decidability.

Description Logic (DL) ontologies often need to model similar properties for different concepts. Taking inspiration from generic classes in object-oriented programming, we introduce concept parameters to describe related concepts. For example, LocalAnesthesia[Eye] and LocalAnesthesia[Knee] can be used to describe the anesthesia of an eye or a knee, respectively. The main benefit of generic concepts is to be able to describe general properties, for example, that every local anesthesia is done by applying an anesthetic drug. We propose to use generic concepts, such as LocalAnesthesia[X] to define such properties, where a concept variable X can be replaced with suitable concepts. To capture the intended meaning of generic concepts, we define two semantics for this extension: the schema semantics, in which concept variables represent arbitrary concepts from a specific language, and the second-order semantics, in which variables represent arbitrary subsets of the domain. Generally, the second-order semantics gives more logical consequences, but the schema semantics allows a reduction to the classical DL reasoning. To combine the benefits of both semantics, we define a useful extension of the DL EL, for which both semantics coincide, and a further restriction in which the entailment problem is decidable.

Abstraction refinement is a recently introduced technique using which reasoning over large ABoxes is reduced to reasoning over small abstract ABoxes. Although the approach is sound for any classical Description Logic such as SROIQ, it is complete only for Horn ALCHOI. In this paper, we propose an extension of this method that is now complete for Horn SHOIF and also handles role- and equality-materialization. To show completeness, we use a tailored set of materialization rules that loosely decouple the ABox from the TBox. An empirical evaluation demonstrates that, despite the new features, the abstractions are still significantly smaller than the original ontologies and the materialization can be computed efficiently.

The paper presents an approach for optimizing the evaluation of SPARQL queries over OWL ontologies using SPARQL's OWL Direct Semantics entailment regime. The approach is based on the computation of lower and upper bounds, but we allow for much more expressive queries than related approaches. In order to optimize the evaluation of possible query answers in the upper but not in the lower bound, we present a query extension approach that uses schema knowledge from the queried ontology to extend the query with additional parts. We show that the resulting query is equivalent to the original one and we use the additional parts that are simple to evaluate for restricting the bounds of subqueries of the initial query. In an empirical evaluation we show that the proposed query extension approach can lead to a significant decrease in the query execution time of up to four orders of magnitude.

Consequence-based ontology reasoning procedures have so far been known only for Horn ontology languages. A difficulty in extending such procedures is that non-Horn axioms seem to require reasoning by case, which causes non-determinism in tableau-based procedures. In this paper we present a consequence-based procedure for ALCH that overcomes this difficulty by using rules similar to ordered resolution to deal with disjunctive axioms in a deterministic way; it retains all the favourable attributes of existing consequence-based procedures, such as goal-directed “one pass ” classification, optimal worst-case complexity, and “pay-asyou-go” behaviour. Our preliminary empirical evaluation suggests that the procedure scales well to non-Horn ontologies. 1

Graded modal logic is the formal language obtained from ordinary modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as "It is true at no fewer than 15 accessible worlds that ...", or "It is true at no more than 2 accessible worlds that ...". We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart-especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.

In this paper, we propose a set of tasks that are relevant for the modular reuse of ontologies. In order to formalize these tasks as reasoning problems, we introduce the notions of conservative extension, safety and module for a very general class of logic-based ontology languages. We investigate the general properties of and relationships between these notions and study the relationships between the relevant reasoning problems we have previously identified. To study the computability of these problems, we consider, in particular, Description Logics (DLs), which provide the formal underpinning of the W3C Web Ontology Language (OWL), and show that all the problems we consider are undecidable or algorithmically unsolvable for the description logic underlying OWL DL. In order to achieve a practical solution, we identify conditions sufficient for an ontology to reuse a set of symbols ``safely''---that is, without changing their meaning. We provide the notion of a safety class, which characterizes any sufficient condition for safety, and identify a family of safety classes--called locality---which enjoys a collection of desirable properties. We use the notion of a safety class to extract modules from ontologies, and we provide various modularization algorithms that are appropriate to the properties of the particular safety class in use. Finally, we show practical benefits of our safety checking and module extraction algorithms.

The ability to extract meaningful fragments from an ontology is key for ontology re-use. We propose a definition of a module that guarantees to completely capture the meaning of a given set of terms, i.e., to include all axioms relevant to the meaning of these terms, and study the problem of extracting minimal modules. We show that the problem of determining whether a subset of an ontology is a module for a given vocabulary is undecidable even for rather restricted sub-languages of OWL DL. Hence we propose two "approximations", i.e., alternative definitions of modules for a vocabulary that still provide the above guarantee, but that are possibly too strict, and that may thus result in larger modules: the first approximation is semantic and can be computed using existing DL reasoners; the second is syntactic, and can be computed in polynomial time. Finally, we report on an empirical evaluation of our syntactic approximation which demonstrates that the modules we extract are surprisingly small.