=Paper=
{{Paper
|id=Vol-477/paper-46
|storemode=property
|title=An Only Knowing Approach to Defeasible Description Logics (extended abstract)
|pdfUrl=https://ceur-ws.org/Vol-477/paper_60.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/LianW09
}}
==An Only Knowing Approach to Defeasible Description Logics (extended abstract)==
https://ceur-ws.org/Vol-477/paper_60.pdf
An Only Knowing Approa h to Defeasible
Des ription Logi s (extended abstra t)
Espen H. Lian and Arild Waaler
Department of Informati s
University of Oslo, Norway,
{elian,arild}ifi.uio.no
1 Introdu tion
We propose the only-knowing logi ORALC , based on the des ription logi ALC .
Only-knowing logi s were originally designed as modal logi s over a lassi al on-
sequen e relation for the representation of autoepistemi reasoning [17, 18℄ and
default logi [15℄. Only-knowing logi s are worth onsidering for several reasons:
They are monotoni logi s with a lear separation between obje t level and
meta level on epts, and they allow faithful and modular en odings of autoepis-
temi and default theories whi h do not in rease the size of the representations.
The en odings thus provide autoepistemi and default logi s with formal seman-
ti s and on eptual larity. Besides being ompletely axiomatized, propositional
only-knowing logi s support en odings of propositional autoepistemi and de-
fault logi s with ni e omputational properties.
{ There is a simple rewrite pro edure that determines extensions. Some of
the rewrite rules are pre onditioned by SAT tests, and these are the only
referen e to meta-logi al on epts in the pro edure.
{ The extension problem for propositional only-knowing logi s have the same
omplexity as for propositional autoepistemi and default logi s.
To our knowledge, no extension of only-knowing logi s to des ription logi s have
yet been given. In this paper we take the des ription logi ALC as the under-
lying logi instead of lassi al propositional logi and generalize the ma hinery
originally designed for propositional logi s of only-knowing. The strength of the
proposed only-knowing logi is the simple rewrite pro edure that it admits for
omputing extensions, and the fa t that reasoning is not harder than in ALC .
The logi ORALC proposed in this paper subsumes the propositional logi that
we proposed in [20℄ and extends that work in a non-trivial way.
The logi ALCK NF introdu ed by Donini, Nardi and Rosati [9℄ is losely
related to ORALC . It is onstru ted by ombining MKNF with ALC . It is not
obvious how this should be done, and in our adaptation of only-knowing logi
to ALC , we have been guided by ALCK . Unlike [9℄, we do not treat so- alled
NF
subje tively quanti ed expressions in this paper but the logi we present is strong
enough to represent, e.g., default theories for ALC .
In [9℄, a tableau pro edure for ALCK is introdu ed. Although the pro e-
NF
dure has been simpli ed [13℄, the pro edure does not seem to be well suited for
omputation of extensions of default theories. In this ase one will, it seems, have
to guess extensions and then use the proof pro edure to he k whether or not
the guess was orre t. In ontrast, the pro edure that we propose determines all
extensions dire tly. Unlike the proof system for ALCK , we formalize inferen e
NF
steps that are suÆ ient for determining extensions but not for hara terizing the
whole semanti s.
2 OR ALC
The language of ORALC is de ned in two steps: rst a on ept language, then
a modal formula language.
Con ept Language. The basis for the on ept language is ALC [1, 29℄:
! > j ? j C j :C j C u D j C t D j 9R :C j 8R :C
C; D at at at
where C is an atomi on ept and R an atomi role. We will all ALC on epts
at at
obje tive on epts. The on ept language for O ALC extends obje tive on epts
R
with modal on ept formation operators1 B (belief) and A (assumption):
C; D !C ALC j :C j C u D j C t D j BC j AC
where C ALC is an obje tive on ept. A modal on ept is of the form BC or AC ;
if C is obje tive, the modal on ept is prime. A on ept is subje tive if every
obje tive sub on ept is within the s ope of a modal on ept formation operator.
An interpretation I = (; ) over onsists of a non-empty domain
I
and an interpretation fun tion mapping atomi on epts and roles to subsets
I
of and resp. Following [9℄ we assume that the domain ontains all
individuals in the language, and that a = a for ea h individual a. Con ept
I
des riptions are interpreted relative to a pair M = (U; V ) and an interpretation
I ; we require that U and V are interpretations over and that V U , but we
do not require that I 2 U . ALC on epts evaluate relative to an I as usual, e.g.,
(:C ) ; = n C ; , while modal on epts are interpreted as follows:
M I M I
\ \
(BC )
M;I
= C M ;J
(AC ) M;I
= C M;J
J 2U J 2V
An ABox A is a nite set of obje tive membership assertions, i.e. on ept asser-
tions C (a) and role assertions R(a; b) for individuals a and b. O is the set of A
individuals expli itly mentioned in A. A modal atom is an assertion of the form
M (a), where M is a modal on ept; M (a) is prime if M is prime. M satis es
C (a) in I if a 2 C ; ; M satis es R(a; b) in I if (a; b) 2 R ; . As we will
M I M I
see, modal atoms play an essential role in the rewrite system. A DBox is a nite
set of terminologi al axioms, i.e. in lusions C v D for on epts C and D, while
1
In the literature, K is sometimes used instead of B, and M instead of A. For: :
intuition about the modalities, onsult the literature about MKNF [9, 22, 23℄ and
only-knowing [15, 20℄.
a TBox is an obje tive DBox. M satis es C v D in I if C ; D ; . We M I M I
de ne a knowledge base (KB) as a tuple (T ; A; D), where T is a TBox, A an
ABox, and D is a DBox. The DBox will typi ally (but not ne essarily) ontain
representation of default rules. We assume standard notions and notations for
default theories. Let , k for 1 6 k 6 n and be ALC - on epts. Below is an
ALC -default and its representation (following Konolige [14℄; note that [9℄ has a
B in front of ) as an in lusion statement:
: 1; : : : ; n = ;
u :A: 1 u u :A: v
B n
B denotes that is believed, while :A: denotes that is onsidered possible,
or that is onsistent with ones beliefs. B is stronger than A in the sense that
every M satis es BC v AC in every interpretation I .
Interpretation of an obje tive on ept is independent of M, hen e we may
write C for C ; and say that I satis es C (a), written I C (a), if a 2 C ;
I M I I
similarly for roles, role assertions and in lusion statements. Hen e we may write
I A and I T if every element in the respe tive ABox and TBox is satis ed
by I . We also write I (T ; A) if I T and I A. For an obje tive assertion ,
we write T ; A if I for every I su h that I (T ; A). Similarly, T ; A A 0
if I A for every I su h that I (T ; A).
0
Formula Language. Formulae are de ned as follows. Con ept and role assertions,
T and F are atomi formulae. :', ' ^ and ' _ are formulae if ' and are.
B, A, B and O are modal operators. B and A orrespond to their on ept
formation operator ounterparts, O is an \only knowing"-operator [17, 33, 20℄,
while B is a \knowing at most"-operator, orresponding to C: of [20℄. L' is a
formula if L is a modal operator and ' is a formula without any o urren e of
. ' is a formula if ' is a subje tive formula, i.e. every atomi formula that
o urs as a subformula in ' is either a subje tive assertion or within the s ope
of a modal operator. Note in parti ular that if C is an obje tive on ept, BC (a)
is a modal atom, and hen e an atomi formula, while B(C (a)) is not an atomi
formula. Abbreviations: ' ) and ' , are de ned as usual; 3 ' is ::';
O ' is O' ^ :O'. Let L be a modal operator. A formula is L-free if it does
R
not ontain L (neither as a modal operator nor as a on ept formation operator)
and L-basi if it is subje tive and ontains no other modality than L.
Relative to the universal set U of all interpretations over that satisfy T ,
a model is a pair (U; V ) su h that V U U . The modality quanti es
over models by means of a binary relation >. Let M = (U; V ). M > M if 0
M = (U ; U ) for some U U ; in whi h ase we say that M is larger than
0 0 0 0
M. Truth onditions are given relative to an interpretation I , whi h needs not
be in V . Atomi formulae and onne tives are interpreted as one would expe t,
e.g., M j= C (a) i a 2 C
I , M j= T and M 6j= F. The modal operators
M;I
I I
are interpreted as follows:
{ M j= B' i M j= ' for ea h J 2 U ;
M j= A' i M j= ' for ea h J 2 V ;
I J
{
M j= B ' i J 2 U for ea h J 2 U su h that M j= ';
I J
{ I J
{ M j= O' i (M j= ' if and only if J 2 U ) for ea h J 2 U ;2
M j= ' i M j= ' for every M > M.
I J
{ I
0
I
0
We write M j= ' if M j= ' for ea h I 2 U . Relative to a model M, k'k
I
M
denotes the truth set of ' in M, i.e. fI 2 U j M j= 'g. Note that if ' is
I
obje tive, k'k is given independently of M, as it only depends on the points
M
in U . For any obje tive ':
{ U = k'k i (U; V ) j= O'; { U k'k i (U; V ) j= B';
{ V k'k i (U; V ) j= A'. { U k'k i (U; V ) j= B
';
Also note that in the lauses that de ne truth for the modal operators, the
interpretation I plays no a tive role in the de nition. When ' is subje tive, it
is immediate that M j= ' i M j= ', i.e. we an safely skip the referen e to
I
I . This is also the reason why the following observation holds.
Lemma 1. For any subje tive on ept M ,
either M j= M (a) , >(a) or M j= M (a) , ?(a).
It is also the ase that M j= ' or M j= :', for any subje tive formula '. A
formula ' is strongly valid, written j ', if M j= ' for every model M. There
is also a weaker notion of validity, whi h is the notion of validity that we are
primarily interested in. It is de ned relative to the set of weak models : (U; V ) is
a weak model if U = V . ' is valid, written j= ', if M j= ' for every weak model
M. Clearly, strong validity implies validity, but not onversely.
Lemma 2. j B' ) A' and j= A' ) B'.
Proof. Follows from the onditions V U (for arbitrary models) and V = U
(for weak models). ut
We are interested in models M of O ', thus we want M to satisfy O' but
R
not 3 O', i.e. no larger model than M should also satisfy O'. The gure below
illustrates the truth onditions relative to M2 > M1 , where M1 = (U1 ; V1 ) for
an obje tive ' and an arbitrary V1 U1 k'k , and M2 = (U2 ; V2 ) = (k'k ; U1 ).
Examining M1 , we see
that U1 k'k , thus
B ' does not hold in M1 ,
hen e neither does O'. U2 = k'k k'k
O' is, however, true in
M2 , and sin e M2 > =
V2 U1
M1 , 3 O' is true in M1 .
Examining M2 , we see
that U2 = k'k , thus O' M2 j= O' ^ :3 O' M1 j= :O' ^ 3 O'
is true. But as there is no
M > M2 that makes O' true, 3 O' is not true. Hen e OR ' holds in M2 .
2
We ould have de ned O in terms of B and B (synta ti ally), as Mj =I O' ,
^
(B' B') but be ause of its spe ial role in the rewrite system, this is not done.
The idea underlying the next lemma an be illustrated with the help of the
model M1 : Any model of 3 O' must have the shape of M1 , in whi h there must
be a point I 62 U1 at whi h ' is true. Note that B' and :B ' are both true
in M1 . Conversely, any model of B' ^ :B ' must also have the shape of M1 ,
satisfying 3 O'.
Lemma 3. j 3 O' , (B' ^ :B ') if ' is obje tive.
For formulae in the A-free fragment of the language, the two notions of validity
oin ide. It is easy to see that in this ase the weak models of OR ' are exa tly
the models (U; U ) with the largest belief state U that satisfy O'.
Let [℄ denote the fun tion that repla es A with B, and (for the servi e of the
rewrite rules) puts the resulting formula on negation normal form, i.e. [A'℄ =
B['℄, [:A'℄ = :B['℄, [::'℄ = ['℄, [:(' ^ )℄ = [:'℄ _ [: ℄, and so forth.
Lemma 4. j 3 ' ) ['℄ if ' is A-basi .
Proof. Let M = (U; V ). If M j= 3 ', then M j= ' for some M > M. By
0 0
de nition, M = (W; U ) for some W U . Sin e ' is A-basi , it is interpreted
0
in M only relative to U . But if we substitute B for all o urren es of A in ',
0
the resulting formula ['℄ is B-basi and is hen e interpreted in M relative to U
in exa tly the same way as ' is interpreted in M . Hen e M j= ['℄.
0
ut
We employ the onvention that when a nite set of formulae X o urs V in pla e
of a formula, this is to be read as the onjun tion of its elements, i.e. X ; for
X = ; this amounts to T. Hen e we will refer to a onjun tion of obje tive
assertions as an ABox. Next we show under whi h onditions OA, for some
ABox A, implies a prime modal atom or its negation. As we will see, this gives
us the side onditions for the ollapse rules in the rewrite system.
Lemma 5. Let C and R be obje tive.
1. j OA ) BC (a) if T ; A C (a);
2. j OA ) :(BC (a)) if T ; A 6 C (a).
Proof. Let M = (U; V ) be a model su h that M j= OA. Then U = kAk . 1.
Assume that T ; A C (a). Then I C (a) for every I s.t. I j= T and I j= A.
Hen e U kC (a)k . It follows that M j= BC (a). 2. Assume that T ; A 6 C (a).
Then I :C (a) for some I s.t. I j= T and I j= A, hen e there is some
interpretation J 2 U \ k:C (a)k . Hen e M j= :(BC (a)). ut
Corollary 1. Let C and R be obje tive.
1. j OA ) AC (a) if T ; A C (a);
2. j= OA ) :(AC (a)) if T ; A 6 C (a)
Proof. By Lemmata 2 and 5. ut
Lemma 6. Let A and A be ABoxes.
0
1. j OA ) B
A if T ; A A.
0 0
2. j OA ) :BA if T ; A 6 A .
0 0
3 The Rewrite System
Generalizing the rewrite system for the underlying propositional language in
[20℄, the system in Fig. 1 onsists of two rewrite relations on formulae. The
rules of the relation are based on strong equivalen es, whereas the ^ relation
extends with rules whose underlying equivalen es are merely weak. We say
that ' redu es to if ' , where is the re exive transitive losure of .
Redu tion an be performed on any subformula. A formula ' is on normal form
wrt. if there is no formula su h that ' . The same notation is used for
the ^ relation. Redu tion is performed modulo ommutativity and asso iativity
of ^ and _, and ' is identi ed with ' ^ T and ' _ F; this implies that T and
F behave as empty onjun tion and disjun tion resp. We de ne to be the set
of rules l r in Fig. 1, while ^ is the union of and the set of rules l ^ r.
Applying the relation exhaustively before the ^ is applied guarantees a orre t
rewrite pro ess.
For formulae and , h=i is a substitution fun tion : 'h=i denotes the
result of substituting every o urren e of in ' with . Substitution is performed
stri tly on the formula level for the reason that assertions do not onsist of
subassertions in the sense that formulae onsist of subformulae. A substitution
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
hM (a)=V (a)i for a prime modal atom M (a) and V 2 f>; ?g is a binding, whi h
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
with this property is obje tive if no prime modal atoms o ur in it. Observe
that the prime modal atom BC (a) has this property, whereas B(C (a)) do not.
Bindings might break this property, e.g., B(BC (a))hBC (a)=>(a)i = B(>(a)).
For this reason we have the M4 rules whi h regain the property, should it be lost
in the ourse of a binding operation, i.e. after the expand rule has been applied:
B(>(a)) (B>)(a). When there are no prime modal atoms left in O', one may
apply the ollapse rules to redu e (or ollapse ) O' ^ M (a) to either O' or F.
The last two rules of C1 are stri tly in ^ . These do not preserve strong
equivalen e and are hen e not sound in all ontexts. Applying the relation
exhaustively to a formula OR ' results in formulae of a form whi h re e ts that
the last two rules of C1 have not been applied. To hara terize this we say that a
formula is semi-normal if it is of the form OA^ for an ABox A and a possibly
empty set of formulae of the form AC (a) and :(AC (a)) with C obje tive and
T ; A 6 :C (a).
Lemma 7. For ea h semi-normal O A ^ ,
1. OA ^ is on normal form wrt. ;
2. either OA ^
^ OA or OA ^ ^ F.
The primary fun tion of the system is to redu e formulae of the form O' and
OR ' for aonjun tion of assertions ', into a disjun tion where ea h disjun t is
Rules for redu ing O
The expand rule:
(M1 )
O' (O'hM (a)=>(a)i ^ M (a)) _ (O'hM (a)=?(a)i ^ :(M (a)))
for any prime modal atom M (a) o urring in '
The domination and distribution rules:
(M2 ) '^F F
(M3 ) (' _ ) ^ (' ^ ) _ ( ^ )
The assertional rules:
:(C (a)) (:C )(a) C (a) ^ D(a) (C u D)(a)
(M4 ) B(C (a)) (BC )(a) C (a) _ D(a) (C t D)(a)
A(C (a)) (AC )(a)
For B = BC (a) and A = AC (a):
OA ^ OA if T ; A C (a)
B OA ^ F if T ; A 6 C (a)
B
OA ^ : F if T ; A C (a) OA ^ : OA if T ; A 6 C (a)
(C1 )
B B
OA ^ OA if T ; A C (a)
A OA ^
^ F if T ; A 6 C (a)
A
OA ^ : F Aif T ; A C (a) OA ^ :
^ OA if T ; A 6 C (a)
A
For an ABox A : 0
OA ^ B A OA if T ; A A
0 0
OA ^ B A F if T ; A 6 A
0 0
(C2 )
OA ^ :BA F if T ; A A
0 0
OA ^ :BA OA if T ; A 6 A
0 0
Rules for redu ing OR and
(R1 ) O' ^ :O'
OR '
(R2 ) :(' _ ) :' ^ :
(R3 ) :F T
(R4 ) :(OA ^ ) :BA _ B A _ [:℄ for semi-normal OA ^
If in rule R4 is empty, we get
(R4 )
0
:OA :BA _ B A
Fig. 1: The rules. A is an ABox, C and D obje tive on epts, and R an obje tive
role. The rules in Ck are alled ollapse rules. R1 is not a proper rule, as the left
hand side is an abbreviation of the right. We in lude it for readability reasons.
of the form O for some obje tive . When ' is the formula representation of
a knowledge base, ea h disjun t represents a Reiter extension of ' (when OR
is used) or an autoepistemi extension (when O is used). To a hieve this, the
rewrite system needs rules for redu ing formulae pre xed with O and :, and
whatever they are redu ed to.
Note that an obje tive formula may or may not be an assertion. C (a) _
:C (a) is, for instan e, not an assertion, but an be transformed to an equivalent
assertion if we \push the a outward" and hange _ to t. Below we address the
reverse operation of \pushing the a inward." We do this to get prime modal
atoms as subformulae, so that the expand rule may be applied. This operation,
JK , is de ned as follows. For role assertions, JR(a; b)K = R(a; b), and for on ept
assertions, JC (a)K = C (a) for C 2 f>; ?g or atomi , and
(
JLC (a)K = LLC (a) if C is obje tive
^ JC (a)K otherwise for L 2 f:; B; Ag;
(
JC ? D(a)K = CJC?(aD)K(a^?)JD(a)K ifotherwise
C ? D is obje tive
for ? 2 fu; tg;
where u^ = ^ and t^ = _, and L^ = L for L 2 f:; B; Ag. In lusions are instanti-
ated and translated into formulae as follows: For an individual a, JC v DKa =
JC (a)K ) JD(a)K .
Example 1. Let us address the default C : > = C , whi h is represented as BC v
C . Let ' = JBC v C K = BC (a) ) C (a). To redu e O', we rst apply the
a
expand rule and then rules from the C1 group. The same redu tions also apply
in a boxed ontext. As the formula is A-free, the
^ relation will not be needed.
:
O( BC (a)_ C (a)) (OC (a) ^ BC (a)) _ (O>(a) ^ :BC (a)) (M1 )
OC (a) _ O>(a) (C1 )
:O(:BC (a) _ C (a)) :(OC (a) _ O>(a))
:OC (a) ^ :O>(a) (R2 )
(:BC (a) _ BC (a)) ^ (:B>(a) _ B>(a)) (R4 )
Having redu ed O' and :O', we redu e O '. R
O ' O' ^ :O'
R
(OC (a) _ O>(a)) ^ (:BC (a) _ B C (a)) ^ (:B>(a) _ B >(a))
(OC (a) ^ (:BC (a) _ B C (a)) ^ (:B>(a) _ B >(a))) _
(O>(a) ^ (:BC (a) _ B C (a)) ^ (:B>(a) _ B >(a))) (M3 )
Distributing onjun tions over disjun tions, using M3 , we obtain a formula on
DNF, whi h redu es to O>(a). This orresponds to the unique Reiter extension.
ut
4 The Modal Redu tion Theorem
The Modal Redu tion Theorem for ORALC states that whenever a formula OR '
en odes a knowledge base, it is logi ally equivalent to a disjun tion, where ea h
disjun t is of the form OA for some ABox A. In fa t, ea h of these disjun ts has
an essentially unique weak model. It is hen e possible, within the logi itself, to
de ompose a formula OR ' into a form whi h dire tly exhibits its models.
We translate an entire knowledge base = (T ; A; D) into a formula as fol-
lows: J KJ = A ^ JDKJ , where JDKJ = fJC v DKa j a 2 J & C v D 2 Dg for
some non-empty set of individuals J . Observe that the TBox T seemingly
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
A1 ; : : : ; A for some n > 0, su h that A A for 1 6 k 6 n, and
n k
j= O J K A , (OA1 _ _ OA ):
R
O n
Proof. By ompleteness (Theorem 1) and soundness (Theorems 2 and 3). ut
We de ne the extensions 3 of to be exa tly the ABoxes A1 ; : : : ; A in The n
Modal Redu tion Theorem. Hen e the notion of extension makes no appeal to
the formula language, only the on ept language.
The rewrite system is just strong enough for establishing the Modal Re-
du tion Theorem: It is sound and omplete for redu tions of OR -formulae into
disjun tions of the appropriate type. It is, however, not omplete for the logi
of OR itself. From the point of view of omputing default extensions this is
enough, be ause only a subset of the logi of OR is a tually needed for the
Modal Redu tion Theorem.
Example 2. The ALC -default Employee : :Manager = Engineer t Mathemati ian
(adapted from [9℄) is represented as BEmployee u :AManager v (Engineer t
Mathemati ian). Let D onsist of this in lusion, and let J = fBob g:
A ^ JDK )
OR ( J
= O (A ^ JBEmployee u :AManager v Eng t MatKBob )
R
= O (A ^ (JBEmployee u :AManager(Bob )K ) JEng t Mat(Bob )K )
R
= O (A ^ (JBEmployee(Bob )K ^ J:AManager(Bob )K ) JEng t Mat(Bob )K )
R
= O (A ^ (BEmployee(Bob ) ^ :AManager(Bob ) ) Eng t Mat(Bob )))
R
This formula an be redu ed to a simpler form, depending on the ABox A and
the TBox. Let T = fManager v Employeeg, and let 1 = BEmployee(Bob ),
2 = AManager(Bob ) and = Engineer t Mathemati ian(Bob ). For any A su h
that A Employee(Bob ), OA ^ 1 OA and OA ^ : 1 F, hen e
O(A ^ ( 1 ^ : 2 ) )) (OA ^ 1 ^ 2 ) _ (O(A ^ ) ^ 1 ^ : 2 ) _
3
Extensions are here taken in the sense of default logi , i.e. Reiter extensions; au-
toepistemi extensions (stable expansions) an be de ned from the Modal Redu tion
Theorem for O in the same way.
(OA ^ : 1 ^ 2 ) _ (OA ^ : 1 ^ : 2 )
(OA ^ 2 ) _ (O(A ^ ) ^ : 2 ):
For the ABox A1 = fEmployee(Bob )g, the redu t is on normal form wrt. but
not for the ABox A2 = fManager(Bob )g:
(OA1 ^ 2 ) _ (O(A1 ^ ) ^ : 2 )
^ O(A1 ^ )
(OA2 ^ 2 ) _ (O(A2 ^ ) ^ : 2 ) OA2
In the former ase, Bob is an engineer or a mathemati ian, in the latter Bob is
only a manager. Redu ing OR (A ^ JDKJ ) produ es the same extensions. ut
4.1 Soundness and Completeness
Lemma 8. For ea h = ( T ; A; D), there is a set 1 = fO(A^Ak ) ^ k g16k6n
of semi-normal formulae for some n > 0 su h that for some set 2 1
_ _
(a) OJ KJ 1 and (b) OR J KJ 2:
Theorem 1 (Completeness). For ea h = (T ; A; D), for some n > 0, there
are ABoxes A1 ; : : : ; An su h that for some set of semi-normal formulae,
_
J K
OR OA ^ (O(A ^ A1 ) _ _ O(A ^ A )):
n
Proof. By Lemmata 7 and 8. ut
Lemma 9. If M j=I ( , ) and does not o ur within the s ope of in ',
then M j=I (' , 'h=i):
The previous result state the ondition under whi h substitution of equivalents
is valid. For substitution within the ontext of we need the stronger notion of
validity. From the point of view of formula rewriting, the signi an e of strong
validity is that it is required for general substitution of equivalents.
Lemma 10. j (' , 'h=i) if j ( , ).
Theorem 2 (Soundness of ). If ' then j ' , .
Proof. By Lemma 10, it is suÆ ient to show that j l , r for ea h rule l r, in
whi h ase we say that the rule is strongly valid. Rule R1 is trivial. R2 follows
from the fa t that j (' ^ ) , (' ^ ) and De Morgan's law, while R3
follows from the fa t that j T. M2 and M3 are propositionally valid, M4 is
left to the reader. C1 follows from Lemma 5 and Corollary 1, while C2 follows
from Lemma 6. The two remaining ases are treated in detail.
R4 : We show that j :(O' ^ ) , ((B' ^ :B ') ) [:℄) for any semi-
normal O' ^ . By Lemma 3, j 3 O' , (B' ^ :B '), hen e by Lemma 10,
we have to show that j :(O' ^ ) , (3 O' ) [:℄). ()) Assume that
M j= (O' ) :) and M j= 3 O'. Then M j= 3 (O' ^:), thus M j= 3 :,
hen e M j= [:℄ by Lemma 4. (() We show that M j= (:O' _ [:℄) )
:(O' ^ ) for every M. Now there are two ases. If M j= :O', then
M j= :(O' ^ ). If M j= [:℄, then M j= :[℄, thus M j= : by Lemma
4, thus M j= :(O' ^ ).
M1 : We show that j O' , (O'hM (a)=>(a)i^ M (a)) _ (O'hM (a)=?(a)i^
:(M (a))) for any prime modal atom M (a). Let M be an arbitrary model.
Then either M j= (M (a) , >(a)) or M j= (M (a) , ?(a)) by Lemma 1. By
Lemma 9, as ' is -free, either M j= O' , O'hM (a)=>(a)i or M j= O' ,
O'hM (a)=?(a)i, resp. In either ase M satis es either (M (a) , >(a)) ^ (O' ,
O'hM (a)=>(a)i) or (M (a) , ?(a)) ^ (O' , O'hM (a)=?(a)i); from whi h
the equivalen e follows. ut
Theorem 3 (Soundness of ^ ). For any disjun tion ' of semi-normal formu-
^ then j= ' , .
lae, if '
Proof. As semi-normal formulae do not ontain , by Lemma 9, it is suÆ ient
to show that j= l , r for ea h rule l ^ r, in whi h ase we say that the rule is
valid. That the rules of are valid is obvious, given that they are strongly valid.
The remaining rules are in the C1 group; validity follows from Corollary 1. u t
4.2 Complexity
The extension problem is determining whether a KB has an extension. A re-
deeming feature of ORALC is that the extension problem is not harder than the
ALC problem of instan e he king.
Theorem 4. The extension problem of OR ALC is PSpa e- omplete.
Proof (Sket h). The translation from to J K A an be done in polynomial
time: jO j jDj. The orresponding extension problem when the underlying
O
logi is propositional is in 2 = NPNP as it an be solved nondeterministi ally
A
p
with a polynomial number of alls to a propositional SAT ora le [33℄. The main
di eren e here is that instead of a SAT ora le, we need an ora le that an
do instan e he ks in ALC , whi h is PSpa e- omplete [1℄. Thus the extension
problem is in NPPSpa e , whi h is equal to PSpa e [25℄. ut
5 Future Work
The underlying on ept language does not have to be ALC . Other on ept lan-
guages with lower omplexity like DL-Lite [4℄ might prove more useful in an
a tual implementation.
An natural extension is to introdu e a partial order (I; 4), intuitively repre-
senting on den e levels, and for ea h index k 2 I , adding modal operators Bk ,
Ak , B k , Ok , and k to the signature of the logi , in order to represent ordered
default theories. Another extension would be allowing subje tively quanti ed ex-
pressions, i.e. on epts of the form 8XR:YC and 9XR:YC for X; Y 2 fB; Ag,
like [9℄ does.
Referen es
1. Baader, F., Calvanese, D., M Guinness, D.L., Nardi, D., Patel-S hneider, P.F.
(eds.): The Des ription Logi Handbook: Theory, Implementation, and Appli a-
tions. Cambridge University Press (2003)
2. Baader, F., Hollunder, B.: Embedding defaults into terminologi al knowledge rep-
resentation formalisms. Journal of Automated Reasoning 14(1), 149{180 (1995)
3. Brewka, G., Eiter, T.: Prioritizing Default Logi . In: Intelle ti s and Computa-
tional Logi , Papers in Honor of Wolfgang Bibel, Applied Logi Series, vol. 19, pp.
27{45. Kluwer A ademi Publishers (2000)
4. Calvanese, D., Gia omo, G.D., Lembo, D., Lenzerini, M., Rosati, R.: DL-Lite:
Tra table Des ription Logi s for Ontologies. In: Pro eedings, The Twentieth Na-
tional Conferen e on Arti ial Intelligen e and the Seventeenth Innovative Appli-
ations of Arti ial Intelligen e Conferen e, (AAAI'05), pp. 602{607 (2005)
5. Chen, J.: Minimal Knowledge + Negation as Failure = Only Knowing (Sometimes).
In: Logi Programming and Non-monotoni Reasoning, Pro eedings of the Se ond
International Workshop, LPNMR 1993, pp. 132{150 (1993)
6. Delgrande, J.P., S haub, T.: Expressing Preferen es in Default Logi . Arti ial
Intelligen e 123, 41{87 (2000)
7. Donini, F.M., Nardi, D., Rosati, R.: Autoepistemi Des ription Logi s. In: Pro-
eedings of the Fifteenth International Joint Conferen e on Arti ial Intelligen e
(IJCAI'97), pp. 136{141 (1997)
8. Donini, F.M., Nardi, D., Rosati, R.: Ground Nonmonotoni Modal Logi s. Journal
of Logi and Computation 7(4), 523{548 (1997)
9. Donini, F.M., Nardi, D., Rosati, R.: Des ription Logi s of Minimal Knowledge and
Negation as Failure. ACM Trans. Comput. Log. 3(2), 177{225 (2002)
10. Engan, I., Langholm, T., Lian, E.H., Waaler, A.: Default Reasoning with Preferen e
within Only Knowing Logi . In: Pro eedings of LPNMR 2005, pp. 304{316 (2005)
11. Gottlob, G.: Translating Default Logi into Standard Autoepistemi Logi . J.
ACM 42(4), 711{740 (1995)
12. Kaminski, M.: Embedding a default system into nonmonotoni logi s. Fundamemta
Informati ae 14(3), 345{353 (1991)
13. Ke, P., Sattler, U.: Next steps for des ription logi s of minimal knowledge and
negation as failure. In: available ele troni ally at CEUR (ed.) Pro . of the 2008
Des ription Logi Workshop (DL 2008) (2008)
14. Konolige, K.: On the relation between default logi and autoepistemi theories.
Arti ial Intelligen e 35(3), 343{382 (1988)
15. Lakemeyer, G., Levesque, H.J.: Only-Knowing: Taking It Beyond Autoepistemi
Reasoning. In: Pro eedings, The Twentieth National Conferen e on Arti ial In-
telligen e and the Seventeenth Innovative Appli ations of Arti ial Intelligen e
Conferen e, AAAI 2005, pp. 633{638 (2005)
16. Lakemeyer, G., Levesque, H.J.: Towards an axiom system for default logi (Pro-
eedings, The Twenty-First National Conferen e on Arti ial Intelligen e and the
Eighteenth Innovative Appli ations of Arti ial Intelligen e Conferen e, AAAI
2006)
17. Levesque, H.J.: All I Know: A Study in Autoepistemi Logi . Arti ial Intelligen e
42, 263{309 (1990)
18. Levesque, H.J., Lakemeyer, G.: The Logi of Knowledge Bases. MIT Press (2001)
19. Lian, E.H., Langholm, T., Waaler, A.: Only Knowing with Con den e Levels: Re-
du tions and Complexity. In: Pro eedings of JELIA'04, Le ture Notes in Arti ial
Intelligen e, vol. 3225, pp. 500{512 (2004)
20. Lian, E.H., Waaler, A.: Computing Default Extensions by Redu tions on OR .
In: Prin iples of Knowledge Representation and Reasoning: Pro eedings of the
Eleventh International Conferen e, KR 2008, pp. 496{506 (2008)
21. Lifs hitz, V.: Nonmonotoni Databases and Epistemi Queries. In: IJCAI, pp.
381{386 (1991)
22. Lifs hitz, V.: Minimal Belief and Negation as Failure. Artif. Intell. 70(1{2), 53{72
(1994)
23. Lin, F., Shoham, Y.: A Logi of Knowledge and Justi ed Assumptions. Artif.
Intell. 57(2-3), 271{289 (1992)
24. Motik, B., Rosati, R.: A Faithful Integration of Des ription Logi s with Logi
Programming. In: M.M. Veloso (ed.) Pro . of the 20th Int. Joint Conferen e on
Arti ial Intelligen e (IJCAI 2007), pp. 477{482. Morgan Kaufmann Publishers,
Hyderabad, India (2007)
25. Papadimitriou, C.M.: Computational Complexity. Addison-Wesley, Reading, Mas-
sa husetts (1994)
26. Reiter, R.: A logi for default reasoning. Arti ial Intelligen e 13(1{2), 81{132
(1980)
27. Rosati, R.: On the de idability and omplexity of reasoning about only knowing.
Artif. Intell. 116(1{2), 193{215 (2000)
28. Rosati, R.: A Sound and Complete Tableau Cal ulus for Reasoning about Only
Knowing and Knowing at Most. Studia Logi a 69(1), 171{191 (2001)
29. S hmidt-S hau, M., Smolka, G.: Attributive on ept des riptions with omple-
ments,. Arti ial Intelligen e 48, 1{26 (1991)
30. Segerberg, K.: Some modal redu tion theorems in autoepistemi logi . Uppsala
Prints and Preprints in Philosophy. Uppsala University (1995)
31. Waaler, A.: Logi al studies in omplementary weak S5. Do toral thesis, University
of Oslo (1994)
32. Waaler, A.: Consisten y proofs for systems of multi-agent only knowing. Advan es
in Modal Logi 5, 347{366 (2005)
33. Waaler, A., Kluwer, J.W., Langholm, T., Lian, E.H.: Only knowing with degrees
of on den e. J. Applied Logi 5(3), 492{518 (2007)