We summarize our recent work [1] on minimal model reasoning in lightweight description logics. Reasoning with minimal models has always been at the core of many non-monotonic formalisms, such as default logic [2], circumscription [3], or answer set programming [4]. Despite it capturing the attention of the KR community over the years, there are still big gaps in our understanding of minimal model reasoning in Description Logics (DLs). When reasoning from a knowledge base, minimal models provide a natural and intuitive counterpart to traditional open-world semantics and classical entailment, which can easily exclude some expected consequences (e.g., a query may be not entailed due to a counter-example model that includes unexpected and unjustified facts). Consider the assertions Under the classical semantics, the inclusion ScandCountry ⊑ NatoMember is not entailed by the above assertions, since there may be unknown Scandinavian countries that are not in NATO. In contrast, considering only those models in which all facts are strictly necessary and justified may lead to more intuitive reasoning, i.e., every Scandinavian country is in NATO. Predicate minimization has been explored in the context of circumscribed DLs , but most existing results spell out the high complexity that results from combining minimized predicates with varying or ifxed predicates; see, e.g., [ 5, 6]. Specifically, when minimized roles and varying predicates are allowed, reasoning becomes quickly undecidable. Except for sporadic results [7, 8], the case of purely minimal models, where nothing can be removed from the extension of any predicate while preserving modelhood, remained largely unexplored. The present extended abstract summarizes our recent work [1]. In [1], we investigate the complexity of reasoning in lightweight DLs in the ℰ ℒ and DL-Lite family under the minimal model semantics, providing the following contributions. ∙ We show that concept satisfiability in a minimal model is undecidable for the DL ℰ ℒ. The decidability status of minimal model reasoning has been open for several years, and the negative outcome is somewhat surprising. Since the reduction does not use the ⊤-concept, the result carries over a restricted class of guarded tuple generating dependencies (TGDs).
∙ We show that decidability can be regained by imposing two simple acyclicity conditions on the TBoxes,
namely strong acyclicity [
We refer to [12] for preliminaries on the DLs studied in this paper. We remark that, unless stated otherwise, we make the unique name assumption (UNA).
Definition 1.
Given two interpretations ℐ and , we let ℐ ⊆ if (i) ∆ ℐ = ∆ and ℐ = , for all ∈ ; (ii) ℐ ⊆ , for all predicates ∈ ∪ .
We write ℐ ⊊ if ℐ ⊆ and ℐ ⊊ for some ∈ ∪ . We call ℐ a minimal model of a KB , if (a) ℐ |= , and (b) there exists no ⊊ ℐ such that |= .
Observe that the relation ⊊ coincides with the preference relation induced by a circumscription pattern
where all predicates are minimized [
Example 1. Take a TBox = {Fan ⊑ ∃likes.Movie Critic ⊑ ∃dislikes.⊤} stating that (movie) fans must like some movie, while critics always dislike something. Consider also ABoxes 1 = {Fan()} and 2 = {Fan(), Critic()}. We are interested in the satisfiability of the concept Movie ⊓ ∃dislikes− .⊤, i.e., the existence of a movie that is disliked by someone. Observe that is not satisfiable in a minimal model of 1 = ( , 1), because 1 has no justification of an object (person) that dislikes something. However, the concept is satisfiable in a minimal model of 2 = ( , 2) (in this model likes a movie that dislikes).
Undecidability. We now state our first and most surprising major result: minimal model reasoning is undecidable already in ℰ ℒ.
Theorem 1. MinModSat in ℰ ℒ is undecidable. This holds even if the ⊤-concept is disallowed. This result, as well as further complexity lower bounds, heavily relies on the flooding technique. Known as saturation in disjunctive logic programming [13], this technique simulates the universal quantification required for minimization, i.e., testing that all substructures are not models. Intuitively, a “flooded” interpretation contains objects that satisfy a given disjunctive concept in more than one way. At the core of this are cyclic dependencies between some concept names 1, 2 that may appear together in some disjunction 1 ⊔ 2 on the right-hand-side of a concept inclusion. Intuitively, verifying that ∈ (1 ⊓ 2)ℐ holds in a minimal model ℐ may require a case analysis: checking that ∈ 1ℐ implies ∈ 2ℐ , and that ∈ 2ℐ implies ∈ 1ℐ . Such case-based verification can be used for testing for crucial properties (errors in a coloring, in a grid construction, etc.), and a flooded minimal model implies that every possible way of avoiding the flooding failed, thus implicitly quantifying over the domain of the structure. As ℰ ℒ concepts do not support disjunctions, another key-ingredient in our proof is the simulation of those. This is achieved by forcing (via minimality) the role successor of an element to point to some individual, and then read-of which one was chosen using existentially qualified concepts.
In our undecidability proof, we rely heavily on cyclic inclusions, and it is thus natural to turn our
attention to acyclic TBoxes, for which minimal model reasoning becomes more manageable.
Strong Acyclicity. Following [
The proof of the lower bound exploits the following example that illustrates how strongly-acyclic ℰ ℒ may require exponentially-large models to satisfy a concept of interest.
Example 2. To generate a binary tree with 2 leaves, consider the assertion L0() and axioms L ⊑ ∃r.L+1 ⊓ ∃l.L+1 for all 0 ≤ < . We want to ensure that all leaves are diferent objects. For this, we add axioms that attempt to produce a second tree starting from its leaves. The latter are identified by concept L′0, which is made available at leaves of the first tree via L ⊑ L′0. Further levels of the second tree, towards its root, are generated with the following axioms for 0 ≤ < :
Left() Right(′)
L′ ⊑ ∃pick.⊤
L′ ⊓ ∃pick.Left ⊑ ∃l′ .L′+1, L′ ⊓ ∃pick.Right ⊑ ∃r′ .L′+1,
L′+1, ⊓ L′+1, ⊑ L′+1 A minimal model can only satisfy the concept L′ if its interpretation of the first tree produces at least 2 instances of L, i.e. of L′0. Indeed, in a minimial model, each element in some L′ has a unique pick-successor , which, in turn, provides with either a unique l′ -successor satisfying L′+1, (if is the interpretation of ), or with a unique r′ -successor satisfying L′+1, (if is the interpretation of ′). Hence, if there are elements satisfying L′+1, then there exist at least 2 elements satisfying L′ . By induction, if L′ is satisfied, then there are at least 2 instances of L′0.
Weak Acyclicity. We also turn to weak acyclicity, which is an important notion for TGDs in the database literature. It relaxes strong acyclicity by annotating some edges in DG ( ) as ⋆-edges, intuitively those witnessing axioms of shape A ⊑ ∃.B, and defining a TBox as weakly-acyclic if there is no cycle in DG ( ) that goes through a ⋆-edge and no node is reachable from ⊤ in DG ( ). We establish a small model property for weakly-acyclic ℰ ℒℐ⊥, which leads to the following result also considering data complexity.
Theorem 3. MinModSat in weakly-acyclic ℰ ℒℐ⊥ is NExpNP-complete. MinModSat for weakly acyclic ℰ ℒℐ⊥ is Σ 2 -complete in data complexity. Lower bounds hold already for ℰ ℒ.
DL-Lite. We do not study the feasibility of MinModSat in the DL-Lite family, but only present one interesting result hinting that the problem will not be easy. In very stark contrast to the previously known NL-membership for MinModSat in DL-Litecore[14], already in DL-Litehornwe have ExpSpacehardness. We hope that this variant and even more expressive extensions like DL-Litebool may be decidable, and plan to look for tight matching complexity bounds.
Theorem 4. MinModSat in DL-Litehorn is ExpSpace-hard.
Tuple Generating Dependencies. ℰ ℒ without ⊤ can be seen as a small fragment of Tuple Generating Dependencies (TGDs), which are prominent in the Database Theory literature (see, e.g., [9, 15]. Thus our lower bounds carry over to minimal model reasoning in TGDs, for problems like brave entailment of an atom, or for checking non-emptiness of a relation in some minimal model of a database and input TGDs. Specifically, an ℰ ℒ TBox without ⊤ can be converted into the so-called guarded TGDs with relations of arity at most 2. Minimal model reasoning over TGDs has been explored in [10], where an undecidability result was achieved using relations of arities up to 4 in the context of the stable model semantics. Our Theorem 1 implies that checking the existence of a stable model for normal guarded TGDs is undecidable already for theories of the form Σ ∪ {¬(⃗) → ⊥}, where Σ has negation-free guarded TGDs with relations of arity ≤ 2, and (⃗) is a ground atom. Similarly, our Σ 2 lower bound in data complexity can be used to improve the Π 2 lower bound in [10] for weakly acyclic TGDs with stable negation. It remains to be explored whether acyclicity conditions and pointwise minimization might also be useful in the richer setting of TGDs.
This work was partially supported by the Austrian Science Fund (FWF) projects PIN8884924, P30873 and 10.55776/COE12.
The authors acknowledge the financial support by the Federal Ministry of Research, Technology and Space of Germany and by Sächsische Staatsministerium für Wissenschaft, Kultur und Tourismus in the programme Center of Excellence for AI-research “Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig”, project identification number: ScaDS.AI
The authors have not employed any Generative AI tools.