with unfoldable Tboxes. Furthermore, the MSC-k
(most-specific concept up to k levels of nested existentials) is supported. In order
to demonstrate the application of these operators, the following knowledge base is
used.
RacerPro 1.9.1 provides a prototypical implementation of the LCS operator (least-common
subsumer) for the description logic with unfoldable Tboxes. Furthermore, the MSC-k
(most-specific concept up to k levels of nested existentials) is supported. In order
to demonstrate the application of these operators, the following knowledge base is
used.
(in-knowledge-base test)
(equivalent x (some r (and a d))) (equivalent y (some r b)) (implies a b) (implies c b) (instance j a) (instance i (all r (and (some r b) d))) (related i j r) (related j k r) (related k i r) |
We no apply the LCS operator to two input concepts.
(lcs-unfold x (and (all r d) (some r c)))
|
The result is (some r (and d b)). If no unfolding is desired, use lcs instead of lcs-unfold. It is possible to specify the Tbox as an optional last argument (default is the current Tbox).
For some purposes, an extract of the information contained in an Abox might be useful. RacerPro 1.9.1 provides an implementation of the MSC-k operator. MSC-k is applied to an individual and a nesting depth. For instance, given the knowledge base above, the following form is executed.
(msc-k i 3)
|
The result is
(and (some r (and a
(some r (and (some r (and (all r (and (some r b) d)) (some r (and a top))))))))) |
It is possible to suppy an additional boolean argument which indicates whether for each individual, the direct types are included in the MSC approximation. For instance,
(msc-k i 3 t)
|
returns
(and (some r
(and x a (some r (and a d y (some r (and *top* (all r (and (some r b) d)) (some r (and x a top))))))))) |
The default for the third argument is nil (indicating that direct types are not to be included in the MSC-k output). Given this boolean argument is specified, there can be a fourth argument, the Abox (which defaults to the current Abox).