Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
On the Convexity and Reliability of the Bethe Free Energy Approximation
The Bethe free energy approximation provides an effective way for relaxing NP-hard problems of probabilistic inference. However, its accuracy depends on the model parameters and particularly degrades if a phase transitio…
The Lindstrom's Characterizability of Abstract Logic Systems for Analytic Structures Based on Measures
In 1969, Per Lindstrom proved his celebrated theorem characterising the first-order logic and established criteria for the first-order definability of formal theories for discrete structures. K. J. Barwise, S. Shelah, J.…
NegationGraph signal interpolation with Positive Definite Graph Basis Functions
For the interpolation of graph signals with generalized shifts of a graph basis function (GBF), we introduce the concept of positive definite functions on graphs. This concept merges kernel-based interpolation with spect…
Truth Set Algebra: A New Way to Prove Undefinability
The article proposes a new technique for proving the undefinability of logical connectives through each other and illustrates the technique with several examples. Some of the obtained results are new proofs of the existi…
Plausible Reasoning about EL-Ontologies using Concept Interpolation
Description logics (DLs) are standard knowledge representation languages for modelling ontologies, i.e. knowledge about concepts and the relations between them. Unfortunately, DL ontologies are difficult to learn from da…