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 languageEnglish
Title of host publicationFrontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Proceedings
EditorsBoris Konev, Giles Reger
PublisherSpringer, Berlin [u. a.]
Pages81-97
Number of pages17
Volume12941
ISBN (electronic)978-3-030-86205-3
ISBN (print)978-3-030-86204-6
Publication statusPublished - 2021
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 12941
ISSN0302-9743

External IDs

ORCID /0000-0002-4049-221X/work/142247978
Scopus 85115241297

Keywords