Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Authors: Timothy S. Lyon, Jonas Karge
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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. |
| Researcher Affiliation | Academia | Tim S. Lyon , Jonas Karge Institute of Artificial Intelligence, Technische Universit at Dresden {timothy stephen.lyon, jonas.karge}@tu-dresden.de |
| Pseudocode | Yes | Figure 1, titled 'The calculus S(O) for the RIQ-ontology O.', presents a uniform presentation of the sequent systems with inference rules. This structured representation serves as an algorithm or procedural definition for the calculus within the context of a theoretical paper. |
| Open Source Code | No | The paper states: 'Although such proofs are in principle computable, we left the specification of an explicit proof-search algorithm that builds such proofs to future work, noting that such algorithms can be written by adapting known techniques'. This indicates that code for the described methods is not yet available. |
| Open Datasets | No | This is a theoretical paper and does not mention or use any datasets for training or evaluation. |
| Dataset Splits | No | This is a theoretical paper and does not involve dataset splits for training, validation, or testing. |
| Hardware Specification | No | This is a theoretical paper and does not mention any hardware specifications used for experiments. |
| Software Dependencies | No | This is a theoretical paper and does not specify any software dependencies with version numbers. |
| Experiment Setup | No | This is a theoretical paper and does not describe any experimental setup details such as hyperparameters or training configurations. |