How many toes do I have? parthood and number restrictions in description logics
Lutz Schröder, Dirk Pattinson · 2008
The modelling of parthood relations in description logics via transitive roles often leads to undecidability when combined with number restrictions and role hierarchies. Here, we in-troduce the description logic PHQ that explicitly supports reasoning about parthood in the presence of qualified number restrictions. Our main results are completeness and decidabil-ity in NEXPTIME. Conceptually, we argue that PHQ pro-vides a better semantic fit for many applications: more often than not, parthoods occurring e.g. in biomedical ontologies are expected to be tree-like. In such cases, PHQ supports stronger inferences than standard description logics. Techni-cally this is achieved by explicitly excluding the merging of descendants, which, at the same time, eliminates the prime source of undecidability. We work in the general setting of coalgebraic modal logic, a generic semantic framework for not-necessarily-normal modal logics. This added generality allows the re-use of many of our results for other logics of sometimes quite different flavour.