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

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

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 any restriction of RIQ, and are applicable to other DLs by suitable modifications.

Details

Original languageEnglish
Title of host publicationProceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI 2024)
EditorsKate Larson
Publisherijcai.org
Pages3484-3492
Number of pages9
ISBN (electronic)9781956792041
Publication statusPublished - 2024
Peer-reviewedYes

External IDs

ORCID /0000-0003-3214-0828/work/199216615
Scopus 85204311576

Keywords

ASJC Scopus subject areas