PaperlayerView exact revision on arXiv

Source-linked AI summary

The Complexity of Circumscription in DLs

Piero A. Bonatti, Carsten Lutz, Frank Wolter

arXiv:1401.3476v1cs.LOcs.AI

TL;DR

Description logics lack defeasible inheritance and default rules, while circumscription’s computational properties for DLs had received little study. The paper analyzes circumscribed DL knowledge bases under restrictions on minimized, fixed, and varying predicates. Concept-only minimization and fixing yields NExpTime^NP-complete reasoning, with a constant predicate bound lowering complexity; role restrictions can instead lead from decidability to undecidability.

  • Problem

    Circumscription’s computational properties in description logics were largely unknown, despite applications needing nonmonotonic features such as defeasible inheritance.

    Source: §1 · p. 2

  • Method

    The paper studies circumscribed knowledge bases, varying which concept and role names are minimized, fixed, or allowed to vary.

    Source: §1 · p. 2

  • Results

    Concept-circumscribed reasoning in ALCIO and ALCQO is NExpTime^NP-complete, dropping to NP^NExpTime-complete with a constant bound on minimized and fixed concept names; role restrictions range from decidability to undecidability.

    Source: §1 · pp. 3–4

  • Takeaways & Limitations

    Restricting minimization and fixing to concept names while allowing roles to vary yields decidable reasoning in expressive DLs, whereas fixing roles can cause very high undecidability.

    Source: §1 · p. 3

    The algorithms rely on massive nondeterministic guessing and therefore do not admit an efficient implementation.

    Source: §8 · p. 41

Abstract

from arXiv · show

As fragments of first-order logic, Description logics (DLs) do not provide nonmonotonic features such as defeasible inheritance and default rules. Since many applications would benefit from the availability of such features, several families of nonmonotonic DLs have been developed that are mostly based on default logic and autoepistemic logic. In this paper, we consider circumscription as an interesting alternative approach to nonmonotonic DLs that, in particular, supports defeasible inheritance in a natural way. We study DLs extended with circumscription under different language restrictions and under different constraints on the sets of minimized, fixed, and varying predicates, and pinpoint the exact computational complexity of reasoning for DLs ranging from ALC to ALCIO and ALCQO. When the minimized and fixed predicates include only concept names but no role names, then reasoning is complete for NExpTime^NP. It becomes complete for NP^NExpTime when the number of minimized and fixed predicates is bounded by a constant. If roles can be minimized or fixed, then complexity ranges from NExpTime^NP to undecidability.

1. Introduction

Description logics lack defeasible inheritance and default rules, despite applications such as exception-rich ontologies and security policies. The paper studies circumscription as an alternative and analyzes the complexity of reasoning under restrictions on which predicates may be minimized or fixed.

1. Introduction

  • The paper addresses a gap in the computational study of circumscribed description logics, as existing nonmonotonic DL approaches mostly use default or autoepistemic logic.The authors note that combining DLs with nonmonotonic logics can create subtle interactions and undecidability risks.Source: §1 · p. 2
  • Circumscription patterns provide defeasible inheritance by transferring class properties to subclasses by default while allowing prioritized exceptions.The paper motivates the approach with biomedical exceptions and incremental security policies.Source: §1 · pp. 2–3
  • Concept-circumscribed reasoning in ALCIO and ALCQO is NExpTime^NP-complete, dropping to NP^NExpTime-complete when the number of minimized and fixed concept names is constant.The lower bound already holds for ALC under specified empty or acyclic TBox and ABox conditions.Source: §1 · p. 3
  • Fixing a single role can make reasoning highly undecidable, while minimizing roles alone preserves decidability for empty-TBox logics between ALC and ALCQO except ALCI and its extensions.For role minimization, adding acyclic TBoxes leads to undecidability.Source: §1 · pp. 3–4
  • Predicate arity and the number of minimized or fixed predicates affect decidability and complexity in ways the authors describe as unusual for nonmonotonic logics.The paper notes a similar boundedness effect in propositional circumscription.Source: §1 · p. 4

2. Description Logics and Circumscription

The section introduces circumscription as a way to model default behavior by preferring models with minimal abnormality, while allowing predicates to be fixed or varied. It formalizes circumscribed knowledge bases and the principal reasoning tasks, and explains how partial priorities can represent specificity.

2. Description Logics and Circumscription

  • The section uses ALC and extensions including number restrictions, inverse roles, and nominals, but excludes ALCQIO because it lacks the finite model property.The upper-bound proofs assume the finite model property, leaving circumscription for logics without that property as an open problem.Source: §2 · p. 5
  • A circumscribed knowledge base inherits the usual DL structure of a TBox for terminological axioms and an ABox for individual assertions.The interpretation-based semantics assigns concepts to domain subsets, roles to binary relations, and individual names to domain elements.Source: §2 · p. 5, §2.2 · p. 9

2.1 Circumscription, Varying Predicates, and Partial Priority Ordering

  • Circumscription restricts inference to models where abnormality predicates are minimized, capturing models that are “as normal as possible.”These preferred models remain classical models of the knowledge base, while permitting additional inferences.Source: §2.1 · p. 6
  • Allowing predicates to vary can support default conclusions that fixed predicates would not yield, as in inferring that a non-whale mammal lives on land.With habitat and Land varying, the example derives that whales are the only mammals not living on land, and hence derives the expected conclusion for Flipper.Source: §2.1 · pp. 6–7
  • Partial priorities between minimized predicates can reflect a partial subsumption hierarchy and give more specific normality information higher priority.For example, staff normality may take priority over user normality because Staff is subsumed by User.Source: §2.1 · p. 8

2.2 Circumscribed Knowledge Bases

  • A circumscription pattern partitions predicates into minimized, fixed, and varying sets, with a strict partial order over the minimized predicates.A cKB combines a TBox and ABox with such a pattern; its models are those for which no preferred model is available.Source: §2.2 · p. 9

Definition 3 (Reasoning tasks)

  • Satisfiability, subsumption, and instance checking are the section’s three central reasoning tasks for circumscribed knowledge bases.The tasks are polynomially reducible to one another, and the paper uses satisfiability as its basic problem.Source: §2.2 · p. 9, Definition 3 (Reasoning tasks) · p. 10

3. Basic Reductions

This section develops reductions for reasoning with circumscribed knowledge bases: simulating fixed concepts, replacing general TBoxes with acyclic ones, and combining certain simultaneous-satisfiability problems into one cKB. The reductions support later complexity analyses and have explicit restrictions, especially for role names.

3. Basic Reductions

  • The section develops three reductions: eliminate fixed concepts, replace general TBoxes with acyclic ones, and reduce certain simultaneous-satisfiability problems to one cKB.The latter reduction requires that the component knowledge bases share no role names.Source: §3 · p. 10, §3.3 · p. 12

3.1 Fixed and minimized concepts

  • Fixed concept names can be eliminated by polynomial reduction, including for ALC cKBs with empty TBoxes and no fixed roles.Fixed role names cannot generally be simulated by minimized roles; some fixed-role reasoning cases are undecidable even when corresponding minimized-role cases are decidable.Source: §3.1 · p. 11

3.2 Acyclic and General TBoxes

  • Satisfiability with general TBoxes reduces in polynomial time to satisfiability with acyclic TBoxes without changing the ABox.For circumscribed KBs, acyclic and general TBoxes have the same complexity; empty TBoxes do not always share that equivalence with non-empty ones.Source: §3.2 · pp. 11–12

3.3 Simultaneous Satisfiability

  • When component cKBs share no role names, their simultaneous satisfiability reduces in polynomial time to satisfiability with a single cKB.The result applies to both circumscribed and concept-circumscribed KBs.Source: §3.3 · p. 12

4. The Complexity of Reasoning in Concept-Circumscribed KBs

This section analyzes the complexity of satisfiability for concept-circumscribed knowledge bases, establishing bounds across ALC, ALCIO, and ALCQO. It also proves ALC hardness results under restrictive conditions and when the number of minimized and fixed predicates is constant.

4.2 Lower Bounds

  • Satisfiability is NExpNP-complete in ALC, ALCIO, and ALCQO when the number of minimized and fixed concept names is unbounded.The section establishes this bound through upper- and lower-bound results.Source: §4 · p. 13, §4.1.1 · p. 15, §4.2 · p. 19

4.1.2 Bounded Number of Minimized and Fixed Predicates

  • With a constant bound on minimized and fixed concept names, satisfiability is NPNExp-complete; subsumption and instance reasoning have co-NPNExp upper bounds.The improved upper bound uses satisfiability of counting formulas as an NExp oracle; counting-formula satisfiability is NExp-complete in ALC, ALCIO, and ALCQO.Source: §4 · p. 13, §4.1.2 · pp. 16, 19

4.1.1 The General Case

  • For concept circumscription without bounds on minimized and fixed predicates, bounded models yield an NExpNP upper bound in ALCIO and ALCQO.The model-size bounds are 2^2n for ALCIO and 2^2n × (m + 1) × n for ALCQO, where m is the largest number-restriction parameter.Source: §4.1.1 · pp. 13–15
  • The bounded-model proof does not extend to minimized or fixed role names, and this limitation is unavoidable because such cases are undecidable.The paper points to undecidability results in Sections 5 and 6.Source: §4.1.1 · p. 15

4.2.1 The General Case

  • The lower bounds already hold in ALC with no fixed predicates or preference relation, via reductions using either an empty TBox and nonempty ABox or an acyclic TBox and empty ABox.The two reductions establish NExpNP hardness for satisfiability in these respective settings.Source: §4.2.1 · p. 19, §4.2 · p. 19
  • A reduction from succinct co-3CERTCOLS encodes its assignment-induced graph and non-3-colorability test as satisfiability in ALC with concept circumscription.The constructed ABox has polynomial size, and the reduction establishes NExpNP-hardness even when the TBox and preference relation are empty and there are no fixed predicates.Source: §4.2.1 · pp. 20, 23
  • Satisfiability in ALC is NExpNP-hard even with an empty TBox and preference relation and no fixed predicates.The same hardness holds with an acyclic TBox, empty ABox and preference relation, and no fixed predicates.Source: §4.2.1 · p. 23

4.2.2 Bounded Number of Minimized and Fixed Predicates

  • With only a constant number of minimized and fixed predicates, ALC satisfiability is NPNExp-hard, even for non-empty TBoxes and empty ABoxes.The proof uses Lemma 8 to separate parts of the reduction; the authors conjecture that the lower bound may also hold for empty TBoxes.Source: §4.2.2 · p. 23
  • The bounded-predicate reduction represents the oracle machine’s computation and its oracle computations in a minimized grid, with results stored for oracle calls.The construction uses TBoxes to describe the machine and oracle computations, and simultaneous satisfiability before applying Lemma 8.Source: §4.2.2 · pp. 24–26
  • Minimizing Rej while all other predicates vary makes Rej true exactly when no accepting computation exists, despite nondeterministic computations and changing grid positions.The construction preserves a grid isomorphic to the original and encodes computations on it, avoiding an unbounded set of fixed coordinate predicates.Source: §4.2.2 · p. 27
  • Satisfiability in ALC is NP^NExp-hard even with an acyclic TBox, empty ABox and preference relations, no fixed predicates, and a constant number of minimized predicates.The theorem states this lower bound for concept-circumscribed cKBs.Source: §4.2.2 · p. 28
  • The authors conjecture the same hardness result for empty TBoxes with non-empty ABoxes; corresponding lower bounds for subsumption and instance problems follow from Section 2’s reduction.Source: §4.2.2 · p. 28

5. Circumscription with Fixed Roles

Allowing role names to be fixed, but not minimized, changes the prior decidability results for concept-circumscribed knowledge bases: reasoning becomes highly undecidable. The paper establishes this by reducing monadic second-order consequence to instance checking, even with empty TBoxes and preference relations.

5. Circumscription with Fixed Roles

  • Before this extension, reasoning with concept-circumscribed knowledge bases had been established as decidable.Source: §5 · p. 29
  • Role-fixing cKBs allow role names to be fixed but not minimized.Source: §5 · p. 29
  • Role-fixing instance checking in ALC is harder than any problem definable in second-order arithmetic, hence outside the analytical hierarchy, even with empty TBoxes and preference relations.The result follows from a reduction of MSO consequence over unrestricted structures; analogous hardness results for satisfiability and subsumption follow from earlier reductions.Source: §5 · pp. 29, 31
  • The reduction proceeds through modal semantic consequence, using Thomason’s result to connect it to MSO consequence.The authors present the proof using the universal role, then adapt it to ALC without the universal role.Source: §5 · pp. 29–31

6. Circumscription with Minimized Roles

The section studies reasoning for role-minimizing circumscribed knowledge bases across DL fragments and TBox settings, reporting NExpNP-completeness for empty-TBox ALCQO and undecidability for empty-TBox ALCI and nonempty-TBox ALC.

6.1 Role-minimizing cKBs With Empty TBox in ALCQO

  • Empty-TBox role-minimizing cKB satisfiability is NExpNP-complete in ALCQO, and remains NExpNP-hard in ALC with just one minimized role and no fixed predicates.Thus, the lower bound holds even with a constant number of minimized predicates.Source: §6.1 · pp. 32–33, §6 · p. 32

6.2 Role-minimizing cKBs With Nonempty TBox

  • With a nonempty TBox, reasoning for role-minimizing cKBs is undecidable already in ALC.The proof reduces the N × N tiling problem.Source: §6.2 · pp. 34, 36

6.3 Reasoning in Role-minimizing cKBs With Empty TBox in ALCI

  • Even with an empty TBox, reasoning for role-minimizing cKBs is undecidable in ALCI.The proof uses inverse roles to simulate TBox reasoning in ABoxes and circumscription to simulate nominals.Source: §6.3 · pp. 36–37
  • Satisfiability with respect to role-minimizing cKBs with an empty TBox is undecidable in ALCI.Source: §6.3 · p. 38

7. Related Work

The section surveys nonmonotonic description-logic approaches, their restrictions, and how they compare with circumscription; a full formal comparison is outside the paper’s scope.

7. Related Work

  • Earlier circumscription work supplied semantics for frames or an effective method for an ALE fragment, but did not analyze complexity or considered only non-prioritized circumscription.The ALE method reduced reasoning to propositional reasoning under the Extended Closed World Assumption.Source: §7 · pp. 38–39
  • Default-logic approaches restrict defaults to named individuals because applying them to anonymous individuals makes reasoning undecidable.This restriction creates an asymmetry because existential quantification commonly produces anonymous individuals in DL models.Source: §7 · pp. 39–40
  • MKNF approaches use restrictions on quantifying-in or on the form of nonmonotonic inclusions to obtain decidability.Their fixed denumerable domain also avoids the named-versus-anonymous individual asymmetry, but finite or varying domains require technical encodings.Source: §7 · p. 40
  • Logic-programming integrations also use negation-as-failure, with some limiting variables to named DL individuals and others using a fixed denumerable domain.The section describes these approaches as related to default- and MKNF-based approaches, respectively.Source: §7 · p. 40
  • MKNF-based approaches do not support specificity-based priorities, which are needed for inheritance mechanisms.The section notes that propositional nonmonotonic logics cannot modularly encode such priorities.Source: §7 · p. 41

8. Conclusions and Perspectives

The paper establishes circumscription as a nonmonotonic DL approach with decidability under suitable restrictions, especially minimizing and fixing concepts while roles vary. It also identifies practical and theoretical limits and further uses for its complexity results.

8. Conclusions and Perspectives

  • Decidability is robust when only concept names are minimized and fixed and all roles vary; with empty TBoxes, minimizing roles remains decidable, but fixing roles does not.The reported bounds for nonempty TBoxes apply to both general and acyclic TBoxes.Source: §8 · p. 41
  • The algorithms rely on massive nondeterministic guessing, and the paper calls for both more efficient methods and guidance for choosing minimized, fixed, and varying predicates.The authors suggest adapting tableau algorithms and possibly hiding abnormality predicates behind explicit defeasible-inclusion syntax.Source: §8 · p. 41
  • Current techniques cover circumscribed DLs with the finite model property; the authors identify more expressive DLs such as SHIQ or OWL as targets for extending results.They also point to circumscribed EL and DL-Lite as a direction toward less expressive DLs.Source: §8 · pp. 41–42
  • The complexity results also yield polynomially reducible links to reasoning about conservative extensions and modularity, providing potential NExpNP lower-bound problems.The paper cites the mutual polynomial reducibility of certain such reasoning services and satisfiability for concept-circumscribed knowledge bases (Konev, Lutz, Walther, & Wolter, 2008).Source: §8 · p. 42

Appendix A. Missing Proofs in Section 3

The appendix proves reductions that remove fixed predicates in ALC satisfiability and combine circumscribed knowledge bases that share no role names. It also establishes a transformation preserving satisfiability between circumscribed knowledge bases.

Lemma 5

  • Lemma 5 reduces ALC satisfiability with concept circumscription, an empty TBox, and no fixed roles to the same problem without fixed predicates.The proof adds fresh concept names and ABox assertions for objects relevant along paths from individuals.Source: Appendix A · pp. 42, 44

Claim 1

  • A countermodel can be restricted to objects reached along relevant paths while preserving the ABox and the failure of the queried assertion.The restricted interpretation is well-behaved for the path mapping used in the proof.Source: Appendix A · p. 43

Lemma 6

  • Lemma 6 equates satisfiability of C0 under the original pattern with satisfiability of C0 ⊓ B′ under a transformed pattern.Source: Appendix A · p. 44

Lemma 8

  • For any description logic in the stated class, simultaneous satisfiability of circumscribed knowledge bases with no shared role names reduces in polynomial time to one circumscribed knowledge base.Source: Appendix A · p. 44

Appendix B. Missing Proofs in Section 4

The appendix establishes a reduction from co-3CERTCOLS to ALC satisfiability under circumscription and derives NExpNP-hardness under restrictive knowledge-base conditions. It also gives a transformation to acyclic TBoxes with empty ABoxes and no fixed predicates.

Lemma 14

  • G is a yes-instance of co-3CERTCOLS exactly when the constructed concept CG is satisfiable under the specified circumscription pattern.Source: Appendix B · p. 46

Corollary 16

  • ALC satisfiability with concept-circumscribed knowledge bases is NExpNP-hard even with an acyclic TBox, empty ABox and preference relation, and no fixed predicates.Source: Appendix B · p. 50

Corollary 16 proof

  • A fresh concept and role convert a single concept assertion into an acyclic TBox, while the construction preserves satisfiability and can eliminate fixed predicates.Source: Appendix B · pp. 50–51

Appendix C. Missing Proofs in Section 5

The appendix reduces MSO(r) logical consequence to instance checking for role-fixing circumscribed knowledge bases in ALC, even with empty TBoxes and preference relations. Its proof uses bounded-neighborhood concepts to approximate universal-role concepts.

Approximation

  • Concepts ∀mR.C approximate ∀u.C using a bounded neighborhood, with the proof taking the bound as 1 + max{2, rd(C)} steps.Source: Appendix C · pp. 51–52

Theorem 22

  • MSO(r) logical consequence effectively reduces to instance checking for role-fixing ALC circumscribed knowledge bases, even with empty TBoxes and preference relations.Source: Appendix C · p. 53

Lemma 31

  • The constructed instance-checking query is equivalent to modal consequence C ⊩ D for the given ALC{r}-concepts.Source: Appendix C · p. 53
Loading 1401.3476v1…