Inproceedings3379: Unterschied zwischen den Versionen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Tim Lyon (Diskussion | Beiträge)
Keine Bearbeitungszusammenfassung
Keine Bearbeitungszusammenfassung
 
Zeile 15: Zeile 15:
|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.
|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.
|Download=IJCAI24-LyoKar.pdf
|Download=IJCAI24-LyoKar.pdf
|Projekt=DeciGUT
|Projekt=DeciGUT, SECAI
|Forschungsgruppe=Computational Logic
|Forschungsgruppe=Computational Logic
}}
}}

Aktuelle Version vom 10. März 2025, 17:53 Uhr

Toggle side column

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

Tim LyonTim Lyon,  Jonas KargeJonas Karge
Tim Lyon, Jonas Karge
Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Proceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI 2024), 2024. ijcai.org
  • KurzfassungAbstract
    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.
  • Projekt:Project: DeciGUTSECAI
  • Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{LK2024,
  author    = {Tim Lyon and Jonas Karge},
  title     = {Constructive Interpolation and Concept-Based Beth Definability
               for Description Logics via Sequents},
  booktitle = {Proceedings of the 33rd International Joint Conference on
               Artificial Intelligence (IJCAI 2024)},
  publisher = {ijcai.org},
  year      = {2024}
}