The language of is dened in two steps: rst a on ept language, then ORALC a modal formula language.
by I. We also write I (T; A) if I T and I A. For an obje tive assertion , every M satises BC v AC in every interpretation I. write for and say that I satises C(a), written I C(a), if a 2 ; CI CM;I CI or that is onsistent with ones beliefs. B is stronger than A in the sense that Interpretation of an obje tive on ept is independent of M, hen e we may if I for every I su h that I (T; A). A0 I A and I T if every element in the respe tive ABox and TBox is satised we write T; A if I for every I su h that I (T; A). Similarly, T; A A0 similarly for roles, role assertions and in lusion statements. Hen e we may write U1
M2 in Conversely, any model of B’ ^ :B’ must also have the shape of M1. M1, that ’ redu es to if ’ , where is the reexiv e transitive losure of . of ^ and _, and ’ is identied with ’ ^ T and ’ _ F; this implies that T and in the ourse of a binding operation, i.e. after the expand rule has been applied: formula is semi-normal if it is of the form OA ^ for an ABox A and a possibly The last two rules of are stri tly in ^ . These do not preserve strong C1 result of substituting every o urren e of in ’ with . Substitution is performed hM (a)=V (a)i for a prime modal atom M (a) and V 2 f>; ?g is a binding, whi h Generalizing the rewrite system for the underlying propositional language in For this reason we have the rules whi h regain the property, should it be lost M4 Applying the relation exhaustively before the ^ is applied guarantees a orre t that the prime modal atom BC(a) has this property, whereas B(C(a)) do not.
B(>(a)) (B>)(a). When there are no prime modal atoms left in O’, one may with this property is obje tive if no prime modal atoms o ur in it. Observe rules of the relation are based on strong equivalen es, whereas the ^ relation of rules l r in Fig. 1, while ^ is the union of and the set of rules l ^ r. the last two rules of have not been applied. To hara terize this we say that a C1 For formulae and , h= i is a substitution fun tion: ’h= i denotes the extends with rules whose underlying equivalen es are merely weak. We say wrt. if there is no formula su h that ’ . The same notation is used for empty set of formulae of the form AC(a) and :(AC(a)) with C obje tive and Redu tion an be performed on any subformula. A formula ’ is on normal form stri tly on the formula level for the reason that assertions do not onsist of exhaustively to a formula results in formulae of a form whi h ree ts that OR’ T; A 6 :C(a). of a value for an assertion C(a) will not apply to, e.g., the assertion C t D(a) but will apply to the equivalent formula C(a) _ D(a). The substitution fun tion [20℄, the system in Fig. 1 onsists of two rewrite relations on formulae. The subassertions in the sense that formulae onsist of subformulae. A substitution rewrite pro ess. equivalen e and are hen e not sound in all ontexts. Applying the relation F behave as empty onjun tion and disjun tion resp. We dene to be the set Bindings might break this property, e.g., B(BC(a))hBC(a)=>(a)i = B(>(a)). apply the ollapse rules to redu e (or ollapse) O’ ^ M (a) to either O’ or F. binds M (a) to V (a).
The expand rule works by binding prime modal atoms in O’, assuming no subformula of ’ is of the form B or A for an obje tive formula . A formula the ^ relation. Redu tion is performed modulo ommutativity and asso iativity a knowledge base, ea h disjun t represents a Reiter extension of ’ (when OR
an essentially unique weak model. It is hen e possible, within the logi itself, to disappears. It does, however, reappear in the side onditions of the ollapse rules. The Modal Redu tion Theorem. For ea h = (T; A; D), there are ABoxes the formula language, only the on ept language. Proof. By ompleteness (Theorem 1) and soundness (Theorems 2 and 3). toepistemi extensions (stable expansions) an be dened from the Modal Redu tion that A F, hen e Mathemati ian). Let D onsist of this in lusion, and let J = fBobg: Theorem for O in the same way. the TBox. Let T = fManager v Employeeg, and let 4 The Modal Redu tion Theorem The rewrite system is just strong enough for establishing the Modal ReWe translate an entire knowledge base = (T; A; D) into a formula as foldu tion Theorem: It is sound and Modal Redu tion Theorem. (adapted from [9℄) is represented as BEmployee u :AManager v (Engineer t disjun t is of the form OA for some ABox A. In fa t, ea h of these disjun ts has tu disjun tions of the appropriate type. It is, however, not omplete for the logi some non-empty set of individuals J . Observe that the TBox T seemingly This formula an be redu ed to a simpler form, depending on the ABox A and Example 2. The ALC-default Employee : :Manager = Engineer t Mathemati ian en odes a knowledge base, it is logi ally equivalent to a disjun tion, where ea h = Engineer t Mathemati ian(Bob). For any A su h