Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents

Tim S. Lyon, Jonas Karge

TL;DR

This is the first sequent-based approach to computing interpolants and definitions within the context of DLs, as well as the first proof that RIQ enjoys the CBP.

Abstract

We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent systems. Using the highly expressive DL RIQ as a case study, we introduce novel sequent calculi for RIQ-ontologies and show how certain interpolants can be computed from sequent calculus proofs, which permit the extraction of explicit definitions of implicitly definable concepts. To the best of our knowledge, this is the first sequent-based approach to computing interpolants and definitions within the context of DLs, as well as the first proof that RIQ enjoys the CBP. Moreover, due to the modularity of our sequent systems, our results hold for restrictions of RIQ, and are applicable to other DLs by suitable modifications.

Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents

TL;DR

This is the first sequent-based approach to computing interpolants and definitions within the context of DLs, as well as the first proof that RIQ enjoys the CBP.

Abstract

We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent systems. Using the highly expressive DL RIQ as a case study, we introduce novel sequent calculi for RIQ-ontologies and show how certain interpolants can be computed from sequent calculus proofs, which permit the extraction of explicit definitions of implicitly definable concepts. To the best of our knowledge, this is the first sequent-based approach to computing interpolants and definitions within the context of DLs, as well as the first proof that RIQ enjoys the CBP. Moreover, due to the modularity of our sequent systems, our results hold for restrictions of RIQ, and are applicable to other DLs by suitable modifications.
Paper Structure (11 sections, 26 theorems, 26 equations, 3 figures)

This paper contains 11 sections, 26 theorems, 26 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Language and Semantics: $\mathcal{RIQ}$
  4. Definability and Interpolation
  5. $\mathbf{R}$-Systems
  6. Sequent Systems
  7. Constructive Sequent-Based Method
  8. Concluding Remarks
  9. Proofs for Section \ref{['sec:log-prelims']}
  10. Proofs for Section \ref{['sec:sequent-systems']}
  11. Proofs for Section \ref{['sec:interpolants']}

Key Result

Lemma 1

If a DL $\mathcal{L}$ enjoys the concept interpolation property, then it enjoys the CBP.

Figures (3)

  • Figure 1: The calculus $\mathsf{S}(\mathcal{O})$ for the $\mathcal{RIQ}$-ontology $\mathcal{O}$. The rules with side conditions $\dag_{1}$ -- $\dag_{5}$ are applicable only if that side condition holds.
  • Figure 2: (Hp-)admissible rules in $\mathsf{S}(\mathcal{O})$. The side conditions are: $\dag_{1}$ = '$x$ is fresh,' $\dag_{2}$ = '$x,y \in \mathrm{Lab}(\Gamma, \Delta)$,' and $\dag_{3}$ = '$x \in \mathrm{Lab}(\Gamma, \Delta)$.'
  • Figure 3: Rules in $\mathsf{SI}(\mathcal{O})$. The $(id_{\dot{=}}^{I})$, $(\forall r^{I})$, and $({\leqslant} n r^{I})$ rules satisfy the same side conditions as $(id_{\dot{=}})$, $(\forall r)$, and $({\leqslant} n r)$, respectively.

Theorems & Definitions (51)

  • Definition 1: Interpretation
  • Definition 2: Concept-Based Beth Definability
  • Definition 3: Concept Interpolation Property
  • Lemma 1
  • Definition 4: $\mathbf{R}$-system
  • Definition 5: Derivation, Language
  • Definition 6: Propagation Graph
  • Definition 7: Propagation Path
  • Example 1
  • Definition 8: Sequent Semantics
  • ...and 41 more