An Introduction to Description Logic by Franz Baader & Ian Horrocks & Carsten Lutz & Uli Sattler

Author:Franz Baader & Ian Horrocks & Carsten Lutz & Uli Sattler [Baader, Franz]
Language: eng
Format: azw3
ISBN: 9780521873611
Publisher: Cambridge University Press
Published: 2017-04-30T04:00:00+00:00

which guarantees that all concept inclusions and global RVMs from T are satisfied.

The proof that D is satisfiable if and only if C is satisfiable with respect to T, which we leave as an exercise, bears some similarity to the proof of Theorem 5.15.

There are not many ways to regain decidability in the presence of role value maps. Note, though, that role hierarchies are a special case of role value maps where sequences of roles are restricted to length one.

5.3.2 Concrete domains

In many applications of DLs, it is also necessary to describe concrete qualities of objects, such as the age of people, which is most appropriately represented by a non-negative integer value. Enabling such representations is the purpose of an extension of Description Logic known as concrete domains. In fact, concrete domains give rise to a class of extensions of a given DL rather than only to a single extension, depending on which concrete qualities we allow to be represented and how we can compare them using predicates. In this section, we show that satisfiability in ALC with general TBoxes becomes undecidable when we add a seemingly simple concrete domain based on the non-negative numbers, with a unary predicate for equality to zero and a binary predicate for incrementation.

A concrete domain is a pair D = (ΔD, ΦD), where ΔD is a non-empty set and ΦD is a finite set of predicates. Each predicate in ΦD has a name P, an arity kP and an extension PD ⊆ (ΔD)kP. The concrete domain used in this section is called D+1. It is defined as ), where consists of the unary predicate =0 associated with the extension and the binary predicate +1 associated with the extension .

To integrate a concrete domain D into a description logic (in this case ALC), we introduce abstract features and concrete features, as additional sorts. Every interpretation I assigns to each abstract feature g a partial function gI : ΔI → ΔI and to each concrete feature h a partial function hI : ΔI → ΔD. Note that an abstract feature is nothing but a role name whose interpretation is restricted to be a partial function. We then add a new concept constructor called a predicate restriction, taking the form ∃c1, . . . , ck.P, where P is the name of a predicate from ΦD of arity k and each ci is a feature chain, that is, a sequence g1 · · · gnh of n ≥ 0 abstract features gi and one concrete feature h. For example, the following GCI expresses that every human has an age and a father who has a larger age:

Human ∃age, father age. >,

where age is a concrete feature, father is an abstract feature and we assume a concrete domain based on the non-negative integers that includes the predicate >. We use ALC(D) to express the extension of ALC with the concrete domain D.

To prove undecidability of satisfiability in ALC(D+1) with respect to general TBoxes, we use a reduction from the halting problem of two-register machines.

Download

Copyright Disclaimer:
This site does not store any files on its server. We only index and link to content provided by other sites. Please contact the content providers to delete copyright contents if any and email us, we'll remove relevant links or contents immediately.