Source-linked AI summary
Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics
Carsten Lutz, Frank Wolter
TL;DR
The paper addresses how to eliminate predicates from ALC TBoxes while preserving consequences over a retained signature, where expressive-DL uniform interpolation is less understood. It develops model-theoretic and automata-theoretic foundations, characterizes interpolants and their existence through bisimulations, and provides decision, computation, size, and conservative-extension results.
Problem
Uniform interpolation and forgetting are useful for ontology reuse, predicate hiding, and summaries, but their behavior is less understood for expressive DLs such as ALC.
Method
The paper combines bisimulation-based model theory with automata-theoretic methods to characterize interpolants, their existence, and related conservative extensions.
Results
The paper obtains semantic characterizations of uniform interpolants and existence, a procedure for computing them when they exist, and size bounds including a triple-exponential upper bound.
Takeaways & Limitations
The framework provides foundations for working with uniform interpolants in expressive DLs and indicates extensions to number restrictions, inverse roles, and fixpoint operators.
Takeaways & Limitations
The resulting algorithm initially has non-elementary running time, and extensions with nominals require more effort.
Abstract
from arXiv · showhide
We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform inter- polants and their existence in terms of bisimula- tions, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model- theoretic and automata-theoretic methods that, as a by-product, also provides characterizations of and decision procedures for conservative extensions.
1 Introduction
The paper frames predicate elimination as forgetting or uniform interpolation, motivated by ontology reuse, predicate hiding, and focused summaries. It establishes foundations for uniform interpolation in expressive DLs, especially ALC, through semantic, algorithmic, and size analyses.
- Motivation: Ontology predicate elimination supports reuse, confidential predicate hiding, and smaller, more focused ontology summaries.These applications remove nonrelevant predicates while preserving the meaning of remaining ones.
- Core notions: Forgetting rewrites a knowledge base without selected predicates while preserving consequences over the remaining predicates.Uniform interpolation is the dual operation, rewriting a formula to a specified signature while preserving consequences expressed in that signature.
- Research gap: Uniform interpolation is comparatively well understood in lightweight DLs, whereas substantially less is known for expressive DLs such as ALC.Prior work offers practical computation in DL-Lite and EL and concept-level results, but the TBox-level expressive-DL situation remains limited.
- Contributions: The paper targets model-theoretic characterizations, existence decisions and computation, and size bounds for uniform interpolants.Its methods combine model theory and automata theory, with conservative extensions also characterized as a by-product.
- Paper organization: Most proofs are deferred to the appendix.
2 Getting Started
This section introduces ALC, uniform interpolants, forgetting, and conservative extensions, then connects uniform interpolation to bisimulation. The resulting characterization supports semantic reasoning about interpolant existence and conservative extensions.
- ALC foundations: ALC concepts use concept and role names with Boolean and existential constructors, and TBoxes are finite sets of concept inclusions.The semantics interprets concepts as domain subsets and roles as binary relations.
- Uniform interpolation and forgetting: A uniform Σ-interpolant preserves exactly the Σ-inclusions entailed by the original TBox while using only the permitted signature.Forgetting a signature is the dual operation of producing a uniform interpolant over the remaining signature.
- Uniform interpolation and forgetting: Uniform interpolants, when they exist, are unique up to logical equivalence.
- Examples: Simple examples show that uniform interpolants may exist, while other ALC TBoxes—including an acyclic EL-TBox—may lack them.The examples include both explicit interpolants and non-existence results.
- Bisimulation: A Σ-bisimulation preserves Σ-concept membership and matches successors in both directions across pointed interpretations.ALCΣ-equivalence is equivalence on all Σ-concepts, and bisimilarity implies it; the converse holds for finite-outdegree interpretations.
- Semantic characterization: Theorem 6 characterizes a uniform interpolant semantically: an interpretation satisfies it exactly when every point is Σ-bisimilar to a point in a model of the original TBox.This characterization is stated using a bisimulation-based existential notation.
- Conservative extensions: The same bisimulation characterization yields a criterion for conservative extensions of TBoxes.Theorem 8 relates conservativity to every point of every model of the base TBox having a suitable bisimilar counterpart.
3 Characterizing Existence of Interpolants
The paper characterizes when finite uniform interpolants exist by analyzing bounded-depth approximations TΣ,m and their bisimulation behavior. It then obtains a single finite test, examples of non-existence and guaranteed existence, and a complexity-aware construction framework.
- Approximation by bounded depth: Infinite TBoxes always provide a uniform Σ-interpolant, but finite interpolants require analyzing the approximations TΣ,m.TΣ,m contains entailed inclusions over finitely representative Σ-concepts of role-depth at most m.
- Bisimulation characterization: An interpretation satisfies TΣ,m exactly when each m-segment is Σ-bisimilar to an m-segment of a model of T.Thus, bounded-depth concepts capture local behavior up to bisimulation, while failures may arise from constraints imposed before the segment.
- Bisimulation characterization: TΣ,m fails to be a uniform interpolant precisely when Σ-information before an m-segment constrains Σ-information after it in a way the segment cannot detect.Theorem 9 expresses this failure through pairs of Σ-tree interpretations and finite-outdegree m-segments.
- Existence and non-existence examples: Forgetting stratified concept names always has a uniform interpolant, and the corresponding TΣ,m provides one.A concept name is stratified when all its occurrences have one fixed nesting depth of existential restrictions.
- Finite decision criterion: The existence test reduces checking all m to one bound: non-existence holds exactly when the condition (∗M2^|T|+1) holds, with MT = 2^2|T|.This finite characterization underlies a decision procedure for uniform interpolant existence.
- Algorithmic consequences: The initial construction is non-elementary in size and running time, but extension sets and a pumping argument support improved procedures.Extension sets capture full types that can extend a Σ-restricted type in models of T; their number is double exponential in |T|.
4 Automata Constructions / Complexity
The paper represents uniform interpolants with alternating parity tree automata and uses them to decide their existence in ALC. This yields a tight 2-EXPTIME-complete existence result and related conservative-extension procedures.
- Automata model: Alternating parity tree automata (APTAs) run on unrestricted interpretations, while their runs remain tree-shaped and use states, transitions, and priorities.Their transitions can test concept names, branch conjunctively or disjunctively, and move along role successors.
- Automata model: APTAs are closed under bisimulation, support polynomial-time complementation and intersection, and have EXPTIME-complete emptiness.These properties make them suitable for encoding the bisimulation-based characterization of uniform interpolants.
- Automata representation: Uniform Σ-interpolants of ALC-TBoxes can be represented by APTAs with 2^O(|T|) states and construction time 2^p(|T|).The automaton accepts pointed Σ-interpretations satisfying the interpolant characterization.
- Decision procedure: An APTA AT,Σ,m recognizes exactly when Condition (∗m) holds, with size exponential in |T| and logarithmic in m.The construction intersects four APTAs, including complementation for one condition.
- Conservative extensions: Conservative-extension checking has a 2-EXPTIME upper bound, with a procedure running in time 2^p(|T|·2^|T′|), and this bound is tight.The paper presents the proof as a more transparent automata-based route to the established upper bound.
- Complexity: 2-EXPTIME is the tight complexity for deciding whether a uniform Σ-interpolant exists for an ALC-TBox.The upper bound follows from the automata construction and emptiness testing, while the lower bound transfers from conservative extensions.
5 Computing Interpolants / Interpolant Size
The paper reduces TBox interpolation to concept interpolation through internalization and derives upper and lower bounds on interpolant size. When a uniform interpolant exists, one can obtain one with a triple-exponential size bound, and matching lower bounds are established.
- Computing interpolants: Concept uniform interpolants can be effectively computed with at most exponential size in the input concept.The paper uses this concept-level result as the basis for constructing TBox interpolants.
- Computing interpolants: TBox interpolation is obtained by internalizing a TBox into a concept and applying concept-level uniform interpolation.The internalization uses a role-depth parameter and then converts the resulting concept back into a TBox.
- Interpolant size: If a uniform Σ-interpolant exists for an ALC-TBox T, then one exists whose size is bounded by a triple-exponential function in |T|.The bound follows from the internalization construction and the exponential concept-interpolant bound.
- Interpolant size: A matching lower bound is obtained from lower bounds for witness concepts associated with non-conservative extensions.The lower-bound family uses a fixed signature of cardinality 4.
6 Conclusions
The paper presents its characterizations, automata tools, and complexity and size results as a foundation for uniform interpolation in expressive description logics. It also discusses possible extensions and application-dependent responses when interpolants do not exist.
- Conclusions: The framework is intended as a general foundation for working with uniform interpolants in expressive description logics.The authors identify the characterizations, tools, and results as the paper’s foundational contribution.
- Extensions: Extending the framework to number restrictions or inverse roles would require modified bisimulations and, for number restrictions, an extended automata model.The paper presents these extensions as feasible with suitable technical modifications.
- Extensions: Extensions involving nominals require more effort than the discussed extensions involving number restrictions or inverse roles.This is the paper’s explicit scope boundary for extending the framework.
- Applications: When a desired interpolant does not exist, ontology reuse and summarization may extend the signature minimally, whereas predicate hiding may not permit that option.The paper suggests using the existence characterization to investigate minimal signature extensions.
A Proofs for Section 2
The proofs connect uniform interpolation with bisimulation through finite-outdegree and modal-saturation arguments. They establish that the relevant Σ-concept consequences are preserved between models related by Σ-bisimulation.
- Example proof: A concrete example shows that A ⊑∃r.(A ⊔¬∃r.A) is a uniform Σ2-interpolant of T2 = {A ≡ B ⊓∃r.B}, with Σ2 = {A,r}.The proof constructs a bisimilar tree interpretation and modifies the interpretation of B while preserving the relevant signature.
- Example proof: The proof transfers the example’s structural properties through Σ2-bisimulation to establish the required entailment relationship.The argument tracks A and r-successor conditions between the original model and a model of T2.
- Bisimulation characterization: For finite-outdegree interpretations, TΣ is a uniform Σ-interpolant of T exactly when its models satisfy the bisimulation-based condition from Theorem 6.The condition relates every pointed interpretation to a pointed model of T through Σ-bisimulation.
- Bisimulation characterization: The ‘if’ direction uses a finite-outdegree countermodel of TΣ and Σ-bisimulation to transfer satisfiability of C ⊓¬D between TΣ and T.This establishes equivalence of Σ-inclusions by preserving Σ-concept truth across bisimilar pointed interpretations.
- Bisimulation characterization: The converse direction uses compactness and modally saturated models to obtain a model of T that is Σ-bisimilar to a given finite-outdegree model of TΣ.Finite subsets of the set of Σ-concepts true at a point are first shown satisfiable, then compactness and modal saturation complete the construction.
B Proofs for Section 3
The proofs characterize uniform interpolation through bounded bisimulations and tree interpretations, then use these characterizations to establish existence criteria, counterexamples, and size bounds.
- B Proofs for Section 3: ALCΣ-m-equivalence is characterized by agreement on all Σ-concepts of role depth at most m.This equivalence is connected to m-bisimilarity, which is defined inductively from atomic agreement and successor matching.
- B Proofs for Section 3: The proof constructs bisimilar tree interpretations by words of paired elements, preserving concept and role interpretations through a finite initial segment and subsequent tree continuation.The resulting interpretations are related to the originals by explicit Σ-bisimulations.
- B Proofs for Section 3: A uniform interpolant candidate TΣ,m fails exactly when two finite-outdegree Σ-tree interpretations satisfy the corresponding bisimulation conditions but disagree on models of T.The construction also preserves finite outdegree through tree-interpretation transformations.
- B Proofs for Section 3: A simple acyclic EL-TBox can lack a uniform interpolant, showing that existence is not guaranteed even in a lightweight description-logic setting.The example uses T4 with signature Σ4 and establishes non-existence through the bisimulation criterion.
- B Proofs for Section 3: If the forgotten symbols are stratified concept names, a uniform interpolant is guaranteed to exist and is given by TΣ,m with m equal to the maximum role depth in T.The proof expands interpretations level by level while preserving the required Σ-reducts.
- B Proofs for Section 3: Theorem 12 reduces non-existence of uniform interpolants to the bounded-depth criterion of Theorem 9 at the bound M_T = 2^2|T|.This replaces an unbounded search over depths with a bound determined by the TBox size.
C Proofs for Section 4
The proofs establish automata-theoretic closure and correctness properties, then use alternating parity tree automata to decide uniform interpolation and conservative extension problems.
- C Proofs for Section 4: The emptiness construction combines dualization with intersection, and both automata transformations are computable in polynomial time in the input automaton size.The dualization swaps Boolean and modal operators and increments priorities, while intersection fuses the component automata.
- C Proofs for Section 4: APTAs are closed under bisimulation: replacing an accepted pointed interpretation by a bisimilar one preserves language membership.The proof transfers an accepting run by recursively matching transition cases in the two interpretations.
- C Proofs for Section 4: APTA emptiness is decidable in time 2^p(||A||), for a polynomial p.The stated result is obtained via a reduction to parity games.
- C Proofs for Section 4: The automaton A_T,Σ accepts exactly the pointed Σ-interpretations that satisfy the existential uniform-interpolation condition for T.The correctness proof extracts a labeled tree run and conversely constructs a model of T from any accepting run.
- C Proofs for Section 4: The constructed automata have |Q| ∈ O(2^O(n) + log^2 m) and |ΣN|, |ΣE| ∈ O(n + log m), where n = |T|.These size bounds support the later complexity analysis for bounded interpolation tests.
- C Proofs for Section 4: Uniform interpolant existence for an ALC TBox and signature is 2-EXPTIME-complete to decide.The same automata-based framework also yields a 2-EXPTIME procedure for conservative extension.
- C Proofs for Section 4: Conservative extension is linked to uniform interpolation by expressing it as the existence of a uniform interpolant for an extended TBox and signature.This gives a reduction between the two decision problems within the framework.
D Proofs for Section 5
The proofs derive a single-concept form for uniform interpolants, establish a doubly exponential lower bound on their size, and use counter constructions based on binary counters and non-violating models.
- D Proofs for Section 5: The construction relies on T_n and T′_n sharing a signature Σ while their remaining symbols are interpreted when extending models.This is the sense in which a model is extended from the original TBox to the combined TBox.
- D Proofs for Section 5: The models of TΣ,n are precisely the interpretations that are not strongly n-violating.This characterization connects the constructed interpolant with the witness-concept argument used for the size lower bound.
- D Proofs for Section 5: The lower-bound contradiction assumes a smaller interpolant, negates it to obtain a witness concept, and contradicts the established witness-size lower bound.The argument uses satisfiability relative to T_n and failure of entailment relative to T_n ∪ T′_n.