The Precise Complexity of Reasoning in $\mathcal{ALC}$ with $ω$-Admissible Concrete Domains (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910462647468032 |
|---|---|
| author | Borgwardt, Stefan De Bortoli, Filippo Koopmann, Patrick |
| author_facet | Borgwardt, Stefan De Bortoli, Filippo Koopmann, Patrick |
| contents | Concrete domains have been introduced in the context of Description Logics to allow references to qualitative and quantitative values. In particular, the class of $ω$-admissible concrete domains, which includes Allen's interval algebra, the region connection calculus (RCC8), and the rational numbers with ordering and equality, has been shown to yield extensions of $\mathcal{ALC}$ for which concept satisfiability w.r.t. a general TBox is decidable. In this paper, we present an algorithm based on type elimination and use it to show that deciding the consistency of an $\mathcal{ALC}(\mathfrak{D})$ ontology is ExpTime-complete if the concrete domain $\mathfrak{D}$ is $ω$-admissible and its constraint satisfaction problem is decidable in exponential time.
While this allows us to reason with concept and role assertions, we also investigate feature assertions $f(a,c)$ that can specify a constant $c$ as the value of a feature $f$ for an individual $a$. We show that, under conditions satisfied by all known $ω$-admissible domains, we can add feature assertions without affecting the complexity. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_19096 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Precise Complexity of Reasoning in $\mathcal{ALC}$ with $ω$-Admissible Concrete Domains (Extended Version) Borgwardt, Stefan De Bortoli, Filippo Koopmann, Patrick Logic in Computer Science Concrete domains have been introduced in the context of Description Logics to allow references to qualitative and quantitative values. In particular, the class of $ω$-admissible concrete domains, which includes Allen's interval algebra, the region connection calculus (RCC8), and the rational numbers with ordering and equality, has been shown to yield extensions of $\mathcal{ALC}$ for which concept satisfiability w.r.t. a general TBox is decidable. In this paper, we present an algorithm based on type elimination and use it to show that deciding the consistency of an $\mathcal{ALC}(\mathfrak{D})$ ontology is ExpTime-complete if the concrete domain $\mathfrak{D}$ is $ω$-admissible and its constraint satisfaction problem is decidable in exponential time. While this allows us to reason with concept and role assertions, we also investigate feature assertions $f(a,c)$ that can specify a constant $c$ as the value of a feature $f$ for an individual $a$. We show that, under conditions satisfied by all known $ω$-admissible domains, we can add feature assertions without affecting the complexity. |
| title | The Precise Complexity of Reasoning in $\mathcal{ALC}$ with $ω$-Admissible Concrete Domains (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2405.19096 |