The question of how a given knowledge base can be modified such that certain unwanted consequences are removed has been investigated in the area of knowledge engineering under the name of repair and in the area of belief change under the name of contraction. Whereas in the former area the emphasis was more on designing and implementing concrete repair algorithms, the latter area concentrated on characterizing classes of contraction operations by certain postulates they satisfy. In the classical setting, repairs and contractions are subsets of the knowledge base that no longer have the unwanted consequence. This makes these approaches syntax-dependent and may result in removal of more consequences than necessary. To alleviate this problem, gentle repairs and pseudo-constractions have been introduced in the respective research areas, and their connections have been investigated in recent work. Optimal repairs preserve a maximal amount of consequences, but they may not always exist. We show that, if they exist, then they can be obtained by certain pseudo-contraction operations, and thus they comply with the postulates that these operations satisfy. Conversely, under certain conditions, pseudo-contractions are guaranteed to produce optimal repairs.
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.
The disjunctive skolem chase is a sound, complete, and potentially non-terminating procedure for solving boolean conjunctive query entailment over knowledge bases of disjunctive existential rules. We develop novel acyclicity and cyclicity notions for this procedure; that is, we develop sufficient conditions to determine chase termination and non-termination. Our empirical evaluation shows that our novel notions are significantly more general than existing criteria.
Minimal Hitting Set (MHS) is a well-known and complete method to compute all minimal explanations of an ABox abduction problem in Description Logics (DL). MHS is NP-complete and generally recognized as inefficient. We leverage on MergeXplain (MXP) which is fast but incomplete – by combining it with MHS in a hybrid algorithm MHS-MXP to regain completeness. In this paper, we describe: (a) the underlying theory to establish the completeness of MHS-MXP and show its relevant properties; (b) a class of inputs on which MHS-MXP has the greatest advantage; (c) an experimental implementation; (d) an empirical evaluation on both favourable and unfavourable inputs.
Dispute resolution is an essential part of argumentation. Although there have been particular advances in computational argumentation with machine learning, we assume that explicit and deterministic techniques for dispute resolution still have significant potential. There are semantic approaches to argument representation, such as the Argument Interchange Format that supports a certain level of interoperability, but according to our knowledge, dispute resolution techniques based on semantics are not yet studied. In this research, we consider single mixed disputes through abstract argumentation frameworks and propose a method for representing such disputes in OWL DL that allows resolving them with reasoning. Additionally, we develop an algorithm for generating the OWL DL representation having argument sets and attack relations as input. The algorithm is validated with a proof of concept implementation, and the OWL DL representation – with an example of correct dispute resolution performed by reasoning over the generated ontology.
