Restricted Unification in the DL 𝓕𝓛₀
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
Unification in the Description Logic (DL) FL0 is known to be ExpTime-complete and of unification type zero. We investigate whether a lower complexity of the unification problem can be achieved by either syntactically restricting the role depth of concepts or semantically restricting the length of role paths in interpretations. We show that the answer to this question depends on whether the number formulating such a restriction is encoded in unary or binary: for unary coding, the complexity drops from ExpTime to PSpace. As an auxiliary result, we prove a PSpace-completeness result for a depth-restricted version of the intersection emptiness problem for deterministic root-to-frontier tree automata. Finally, we show that the unification type of FL0 improves from type zero to unitary (finitary) for unification without (with) constants in the restricted setting.
Details
Original language | English |
---|---|
Title of host publication | Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Proceedings |
Editors | Boris Konev, Giles Reger |
Publisher | Springer, Berlin [u. a.] |
Pages | 81-97 |
Number of pages | 17 |
Volume | 12941 |
ISBN (electronic) | 978-3-030-86205-3 |
ISBN (print) | 978-3-030-86204-6 |
Publication status | Published - 2021 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 12941 |
---|---|
ISSN | 0302-9743 |
External IDs
ORCID | /0000-0002-4049-221X/work/142247978 |
---|---|
Scopus | 85115241297 |