Collaborating Authors

Koopmann, Patrick

Efficient TBox Reasoning with Value Restrictions using the $\mathcal{FL}_{o}$wer reasoner Artificial Intelligence

To define the important notions of such an application domain as formal concepts, DLs state necessary and sufficient conditions for an individual to belong to a concept. These conditions can be Boolean combinations of atomic properties required for the individual (expressed by concept names) or properties that refer to relationships with other individuals and their properties (expressed as role restrictions). For example, the concept of a parent that has only daughters can be formalized by the concept description C: child.Human child.Female, which uses the concept names Female and Human and the role name child as well as the concept constructors conjunction (), existential restriction ( r.D), and value restriction ( r.D). Constraints on the interpretation of concept and role names can be formulated as general concept inclusions (GCIs). For example, the GCIs Human child.Human and child.Human Human say that humans have only human children, and they are the only ones that can have human children. DL systems provide their users with reasoning services that allow them to derive implicit knowledge from the explicitly represented one.

Signature-Based Abduction with Fresh Individuals and Complex Concepts for Description Logics (Extended Version) Artificial Intelligence

Given a knowledge base and an observation as a set of facts, ABox abduction aims at computing a hypothesis that, when added to the knowledge base, is sufficient to entail the observation. In signature-based ABox abduction, the hypothesis is further required to use only names from a given set. This form of abduction has applications such as diagnosis, KB repair, or explaining missing entailments. It is possible that hypotheses for a given observation only exist if we admit the use of fresh individuals and/or complex concepts built from the given signature, something most approaches for ABox abduction so far do not support or only support with restrictions. In this paper, we investigate the computational complexity of this form of abduction -- allowing either fresh individuals, complex concepts, or both -- for various description logics, and give size bounds on the hypotheses if they exist.

Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report) Artificial Intelligence

Logic-based approaches to AI have the advantage that their behavior can in principle be explained to a user. If, for instance, a Description Logic reasoner derives a consequence that triggers some action of the overall system, then one can explain such an entailment by presenting a proof of the consequence in an appropriate calculus. How comprehensible such a proof is depends not only on the employed calculus, but also on the properties of the particular proof, such as its overall size, its depth, the complexity of the employed sentences and proof steps, etc. For this reason, we want to determine the complexity of generating proofs that are below a certain threshold w.r.t. a given measure of proof quality. Rather than investigating this problem for a fixed proof calculus and a fixed measure, we aim for general results that hold for wide classes of calculi and measures. In previous work, we first restricted the attention to a setting where proof size is used to measure the quality of a proof. We then extended the approach to a more general setting, but important measures such as proof depth were not covered. In the present paper, we provide results for a class of measures called recursive, which yields lower complexities and also encompasses proof depth. In addition, we close some gaps left open in our previous work, thus providing a comprehensive picture of the complexity landscape.

Signature-Based Abduction for Expressive Description Logics -- Technical Report Artificial Intelligence

Signature-based abduction aims at building hypotheses over a specified set of names, the signature, that explain an observation relative to some background knowledge. This type of abduction is useful for tasks such as diagnosis, where the vocabulary used for observed symptoms differs from the vocabulary expected to explain those symptoms. We present the first complete method solving signature-based abduction for observations expressed in the expressive description logic ALC, which can include TBox and ABox axioms, thereby solving the knowledge base abduction problem. The method is guaranteed to compute a finite and complete set of hypotheses, and is evaluated on a set of realistic knowledge bases.

Small Is Beautiful: Computing Minimal Equivalent EL Concepts

AAAI Conferences

Rudolph 2012; Lutz, Seylan, and Wolter 2012), ontology Logics allow equivalent facts to be expressed in many different learning (Konev, Ozaki, and Wolter 2016; Lehmann and ways. The fact that ontologies are developed by a Hitzler 2010), rewriting ontologies into less expressive logics number of different people and grow over time can lead to (Carral et al. 2014; Lutz, Piro, and Wolter 2011), concepts that are more complex than necessary. For example, abduction (Du, Wang, and Shen 2015; Klarman, Endriss, below is a simplified definition of the medical concept and Schlobach 2011), and knowledge revision (Grau, Kharlamov, Clotting from the Galen ontology (Rector et al. 1994): and Zheleznyakov 2012; Qi, Liu, and Bell 2006).

Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes

AAAI Conferences

Uniform interpolation and the dual task of forgetting restrict the ontology to a specified subset of concept and role names. This makes them useful tools for ontology analysis, ontology evolution and information hiding. Most previous research focused on uniform interpolation of TBoxes. However, especially for applications in privacy and information hiding, it is essential that uniform interpolation methods can deal with ABoxes as well. We present the first method that can compute uniform interpolants of any ALC ontology with ABoxes. ABoxes bring their own challenges when computing uniform interpolants, possibly requiring disjunctive statements or nominals in the resulting ABox. Our method can compute representations of uniform interpolants in ALCO. An evaluation on realistic ontologies shows that these uniform interpolants can be practically computed, and can often even be presented in pure ALC.