Ex ension o On ologies Assis ed by Au oma ed
Reasoning Sys ems
Joaqu´ın Bo ego-D´ıaz and An onia M. Ch´a ez-Gonz´alez
Depa amen o de Ciencias de la Compu aci´on e In eligencia A ificial,
E.T.S. Ingenie ´ıa In o m´a ica-Uni e sidad de Se illa,
A da. Reina Me cedes s.n. 41012-Se illa. Spain
Abs ac . A me hod o ex end on ologies wi h he assis ance o au-
oma ed easoning sys ems and p ese ing a kind o comple eness wi h
espec o hei associa e concep ualiza ions is p esen ed. The use o such
sys ems makes easible he on ological inse ion o new concep s, bu i
is necessa y o e-in e p e he olde ones wi h espec o new on ological
commi men s. We illus a e he me hod ex ending a well-known on ology
abou spa ial ela ionships, he called Region Connec ion Calculus.
1 In oduc ion
On ology Managemen has becomed in a c i ical issue in fields ela ed wi h
Knowledge Rep esen a ion and in elligen in o ma ion p ocessing as he Seman-
ic Web. One o he in ol ed asks, he mos impo an , is he need o ex ending
o e ising on ologies. This ask may be, om he poin o iew o companies,
dange ous and expensi e: e e y change in he on ology can affec o he o e all
knowledge o ganiza ion o he company. Mo eo e i is also known ha he sel
p ocess o ex ension is ha d o au oma ize: he ools a e designed o acili a e
he syn ac ic ex ension o on ology mapping. Bu he effec o on ology mapping
on he logical easoning may be, in gene al, unknown, and specially on he use
o au oma ed easoning sys ems [2].
The aim o his pape is o p opose a o mal seman ics o on ology ex en-
sion ( ollowing he ounda ional p inciples gi en in [2] and sugges ed by he
compu e -assis ed cleaning o Knowledge Da abases [1]) as well as a easible
me hod, assis ed by Au oma ed Reasoning Sys ems (ARS), o ex end on ologies
p ese ing a ce ain ype o obus ness.
2 La ice Ca ego ical Ex ensions
We assume h oughou ha he concep ualiza ion associa ed o he on ology is
endowed o la ice s uc u e. Ac ually i is no a cons ain : he e a e me hods
Pa ially suppo ed by he p ojec TIN2004-03884 o Spanish Minis y o Educa ion
and Science, cofinanced by FEDER unds.
o ex ac la ices o concep s om da a (such as he Fo mal Concep s Analysis,
see e.g. [8]), and an on ology is easy o be ex ended by defini ion o sa is y
i . Al hough we hink abou Desc ip ion Logics as a language (a logical basis
o on ology languages like OWL, see h p://www.w3.o g/TR/owl- ea u es/),
he amewo k is use ul o Fi s O de Logic (FOL).
Ala ice ca ego ical heo y is a heo y ha p o es he la ice s uc u e o i s
basic concep s. I is a easonable equi emen : he heo y mus ce i y he basic
ela ionships among hem. We aim o eplace comple eness by la ice ca ego ici y
o make easible he ex ension o o mal on ologies.
Fixed a language, le C={C1,...,C
n}be a se o concep symbols and le T
be a heo y (in he gene al case, definable concep s in Tcanbeassumed)andle
us conside he language LC={,⊥,≤}∪{c:c∈C}.Gi enM|=T,wecon-
side he LC-s uc u e L(M,C), whose uni e se is he se o he in e p e a ions
in Mo he concep s (is M,⊥is ∅), and ≤is he subse ela ion.
The ela ionship be ween L(M,C)and hesel Mis based in wo ac s. The
fi s one, ha he la ice can be cha ac e ized by a fini e se o equa ions E,
plus a se o o mulas ΘCca ego izing he la ice unde comple ion, ha is, ΘC
includes he domain closu e axiom, he unique names axioms and adi ionally
he axioms o la ice heo y. Secondly, he e is a na u al ansla ion Πo la ice
equa ions in o FOL o mulas such ha i Eis a se o equa ions cha ac e izing
L(M,C), hen M|=Π(E).
Defini ion 1. We say ha a LC- heo y Eis a la ice skele on (l.s.) o Ti
–The e is M|=Tsuch ha L(M,C)|=E+ΘC,and
–E+ΘChas an only model (modulo isomo phism).
E e y consis en heo y Thas a la ice skele on (i is sufficen o ca ego ically
axioma ize he la ice associa ed o some model o T). In ui i ely, he exis ence
o essen ially diffe en la ice skele ons difficul s he easoning wi h he concep-
ualiza ion associa e o T.
Defini ion 2. Tis called a la ice ca ego ical (l.c.) heo y i wha e e wo
la ice skele ons o Ta e equi alen modulo ΘC.
I is easy o see ha e e y Tconsis en has a la ice ca ego ical ex ension:
i is sufficen o conside a model M|=T, and nex o find a se Eo equa ions
such ha ΘC+Ehas L(M,C) as only model. The heo y T+Π(E)(andany
consis en ex ension o i ) is l.c.
To simpli y, we deal wi h a pai (T,E)-whe eTis la ice ca ego ical and E
is a la ice sekele on o T- ha wecallala ice ca ego ical co e (l.c.c.). Thus,
(T,E) is a l.c.c. i T+Π(E) is a l.c. heo y.
Defini ion 3. Gi en wo l.c.c. (T1,E
1),(T2,E
2)wi h espec o he se s o con-
cep s C1and C2 espec i ely, we say ha (T2,E
2)is a la ice ca ego ical ex-
ension o (T1,E
1)i L(T1,C1)⊆L(T2,C2)and L(T2,C2)|=E1.
3 Ex ending On ologies
In o de o ob ain a p ac ical me hod, some o he basic ( heo e ical) logical p in-
ciples equi ed by he defini ional me hodologies o building o o mal on ologies
mus be weakened [3]. Such p inciples, in hei o iginal o ms, a e:
1. On ologies should be based upon a small numbe o p imi i e concep s.
2. These p imi i es should be gi en defini e model heo e ic seman ics.
3. Axioms should only be gi en o he p imi i e concep s.
4. Ca ego ical axiom se s should be sough .
5. The emaining ocabula y o he on ology (which may be e y la ge), should
be in oduced pu ely by means o defini ions.
The h ee fi s p inciples a e assumed, bu , in o de o a easible managemen ,
he las wo ones ( wo s ong logical cons ain s) a e weakened. The ou h one
will be eplaced by la ice ca ego ici y, mo e manageable han logical ca ego ici y
o comple eness. Wi h espec o he las one, i we s a wi h a basic heo y, i
can be ha d o define any new concep / ela ion by means o he basic elemen s o
he on ology. Thus, we mus conside ha he e a e on ological inse ions, ha
is, addi ions o new concep s/ ela ions no on ologically defined on he o me
on ology. This may p oduce a deep eadd ess o he domain analysis.
The me hod consis s o ou s eps, assis ed by an au oma ed heo em p o e
(in ou case, OTTER, h p://www-unix.mcs.anl.go /AR/o e /), a model
finde (MACE4, www-unix.mcs.anl.go /AR/mace4/), and a las s age o on-
ological econside a ion. S a ing om a la ice ca ego ical heo y:
1. Fi s , one ex ends he la ice o he basic concep s o he on ology by ex-
ending he selec ed skele on.
2. Nex , one applies MACE4 on a possible axioma iza ion o he new la ice
in o de o ob ain he new la ices. In gene al, he cha ac e iza ion o he
la ice is a heo y weake han he ini ial on ology.
3. The hi d s ep consis s o he efinemen o he skele on in o de o MACE4
exhibi s one only model ( ha is, he heo y is la ice ca ego ical).
4. Finally, i is necessa y o ce i y (by means OTTER o hand-made) he
unici y o abo e model.
The final s age o he me hod is no algo i hmical. I consis s o an on ological in-
e p e a ion o he new elemen , by e-in e p e ing (gene ally by efining) i nec-
essa y, he olde ones. This ask, nonalgo i hmical in essence, is esponsabili y o
expe s in he domain ep esen ed by he on ology. In ac , such e-in e p e a ion
can o ce us o econside he ini ial on ological commi men s.
4 An Example in Quali a i e Spa ial Reasoning
We shall apply he me hod o ex ending an on ology on Quali a i e Spa ial
Reasoning by means o he inse ion o ela ions on impe ec spa ial in o ma-
ion, conc e ely he well-known Region Connec ion Calculus (RCC) [6]. The
DC(x, y)↔¬C(x, y)(xis disconnec ed om y)
P(x,y)↔∀z[C(z,x)→C(z,y)] (xis pa o y)
PP(x,y)↔P(x, y)∧¬P(y,x)(xis p ope pa o y)
EQ(x, y)↔P(x, y)∧P(y,x)(xis iden ical wi h y)
O(x, y)↔∃z[P(z,x)∧P(z,y)] (xo e laps y)
DR(x,y)↔¬O(x, y)(xis disc e e om y)
PO(x,y)↔O(x, y)∧¬P(x, y)∧¬P(y,x)(xpa ially o e laps y)
EC(x, y)↔C(x, y)∧¬O(x, y)(xis ex e nally connec ed o y)
TPP(x,y)↔PP(x, y)∧∃z[EC(z,x)∧EC(z,y)] (xis a angen ial p op. pa o y)
NTPP(x, y)↔PP(x, y)∧¬∃z[EC(z,x)∧EC(z,y)] (xis a non- ang. p op. pa o y)
Fig. 1. Axioms o RCC
≡CDR PO¬P¬Pi¬DR DR≡EC DC
NTPP¬TPP ¬Pi¬DR C≡OEC TPP¬Pi¬DR
O≡POPPi EQ¬PPi¬DR Pi≡EQ PPi
TPPi¬NTPPi¬DR P≡EQ PP NTPPi¬DR
PPi≡TPPiNTPPi EC¬DC PP≡TPP NTPP
Fig. 2. The skele on E o he la ice o concep s o RCC
need o such ex ension a ose, o example, when we applied RCC as a me a-
on ological ool o analysing and epai ing anomalies in on ologies [1] [5]. RCC
is a me eo opological app oach o spa ial easoning; he spa ial en i ies a e non-
emp y egula se s. The p ima y ela ion is he connec ion,C(x, y), wi h in-
ended meaning: “ he opological closu es o xand yin e sec ” and basic axioms
∀x[C(x, x)] and ∀x, y[C(x, y)→C(y,x)] join ly wi h a se o defini ions on he
main spa ial ela ions (fig. 1). Ac ually he heo y has o he axioms (see [6]),
bu hese a e no necessa y o p o e he la ice s uc u e o he se o ela ions
(shown in fig. 3). Thus, RCC is la ice ca ego ical.
4.1 Isola ing a Skele on o RCC
In o de o isola e a skele on wi hou edundan o mulas, we s a wi h he
la ice equa ions induced by he Hasse diag am o he RCC- ela ions. Nex we
sequen ially emo e equa ions o his se when such elimina ion does no p oduce
o he new la ices modelling he final se . The se o equa ions E,see hefigu e
2, we ob ain has an only model (is a skele on). ca ego izes unde comple ion he
la ice o he RCC-spa ial ela ionships (gi en in fig. 3) [5].
4.2 Inse ing New Elemen s
The Join ly Exhaus i e and Pai wise Disjoin se (JEPD) o a omic ela ions
o he la ice (fig. 3) is deno ed by RCC8. I ep esen s he se o he mos
specific spa ial ela ions in RCC8. Ou aim is o inse a new ela ion ep esen ing
undefini ion, such ela ion mus be disjoin wi h RCC8.
12345678
910
1211
13
14 15
16
PP
PO TPP EQ EC DCTPPi NTPPi
PPi
PiP
O
CDR
NTPP
0
aba
ba
b
a b a
bb
a
ab
a
b
yolk
egg
Fig. 3. The la ice o RCC- ela ions (le ) and he egg-yolk ep esen a ion o ague
egions ( igh )
Theo em 1. The e a e only eigh E-conse a i e ex ensions o he la ice o
RCC by inse ion o a new ela ion Dsuch ha RCC8∪{D}is a JEPD se .
In he p oo o he heo em we use MACE4 o lis ing he la ice ex ensions,
aking as inpu he la ice axioms, he skele on, he unique names p inciples and
he closu e domain axiom. The sys em ou pu s eigh ex ensions. Since MACE4
has no been o mally e ified o wo k co ec ly, i is necessa y o ce i y ha
such models a e co ec , and, by finding OTTER’s p oo s, o show ha he lis
o models is exhaus i e. The analysis o he ex ensions (fig. 4) sugges s us ha
he new ela ions ep esen undefini ion up o a deg ee.
4.3 Refining he Skele on o he New Ex ension
We a e no specially in e es ed he e in a de e mina ed ex ension, al hough he e
exis si ua ions whe e i is necessa y o selec one o hem (by example, when we
in end o classi y unaccu a e da a [4]). Howe e , he efinemen o he skele on
is easy: once an ex ension is selec ed. Fo ins ance, wi h espec o he fi s
ex ension, i is sufficen o subs i u e he o mula PP ≡TPP NTPP by he
new o mula PP ≡TPPI1NTPP o ob ain a skele on E o he ex ension.
E e y ex ension o (RCC, E) is a l.c. ex ension o (RCC, E).
4.4 Final S age: On ological In e p e a ion
Finally, we need o me eo opologically in e p e he new ela ions. In [5] ou
diffe en in e p e a ions a e offe ed, we ied o use some o hem o suppo ing
CDR
O
PPi
PP PPi
EC DCPO NTPP TPP EQ TPPi NTPPi
I
CDR
O
PPi
PP PPi
EC DCPO NTPP TPP EQ TPPi NTPPi
I
CDR
O
PPi
PP PPi
ECPO NTPP TPP NTPPiEQ TPPi DC
I
CDR
O
PPi
PP PPi
ECTPPiPO DCNTPP TPP EQ NTPPi
I
CDR
DC
O
P
PPi
TPPi NTPPiEQTPPPO
Pi
PP
NTPP EC
I
CDR
DC
PP
ECNTPPPO TPP EQ
O
PPi
PPi
NTPPiTPPi I
CDR
PP
NTPPPO TPP EQ
O
PPi
PPi
NTPPiTPPi EC DC I
C
PP
NTPPPO TPP EQ
O
PPi
PPi
NTPPiTPPi EC DC
DR
I
Fig. 4. The eigh la ice desc ibing he l.c. ex ensions o RCC by undefini ion
on ological cleaning asks. In o de o show how hey can be in e p e ed in each
case, we conside he classical egg-yolk in e p e a ion o spa ial ague egions
[7]. In ui i ely, a spa ial egion acompounded by wo sub egions, as figu e 3
shows, he fi s , y(a)( he yolk) which ep esen s accu a e loca ions in a,and he
second one, e(a) bounding he unaccu a e loca ions o a. In [7] he 48 possible
spa ial ela ions be ween wo ague egions a e shown. I we wan o wo k wi h
I1, o example, i s ague in e p e a ion is I1(a, b)≡PP(e(a),e(b)), while RCC
ela ions a e in e p e ed by he na u al way.
5FinalRema ks
The me hod desc ibed he e is a logical basis o ex ending on ologies. Since
he e is a lack o o mal no ions - easible in p ac ice- desc ibing ea u es abou
comple eness in he e olu ion o o mal on ologies, we hink ha ou p oposal
can be use ul o add o mal seman ics o se e al on ological ans o ma ions [5]
[1], achie ing in his way he logical us . The easibili y o he me hod depends
o wo ac o s: he use o efficen ARS and he simplici y o he comple eness
no ion, ela ed wi h he concep ualiza ion o he on ology. Fu u e esea ch lines
a e add essed o emb ace he use o oles on spa ial easoning.
Re e ences
1. J. A. Alonso-Jim´enez, J. Bo ego-D´ıaz and A. M. Ch´a ez-Gonz´alez, On ology Clean-
ing by Me eo opological Reasoning P oc. o DEXA Wo kshop on Web Seman ics
(WebS’04), (2004). IEEE P ess, pp. 132-137.
2. J. A. Alonso-Jim´enez, J. Bo ego-D´ıaz, A. M. Ch´a ez-Gonz´alez and F.J. Ma ´ın-
Ma eos, Founda ional challenges in Au oma ed and On ology Cleaning in he Se-
man ic Web. To appea in IEEE In elligen Sys ems.
3. B. Benne , The Role o Defini ions in Cons uc ion and Analysis o Fo mal On olo-
gies, in: P. Dohe y, J. McCa hy, and M. Williams (eds.) Logical Fo maliza ion o
Commonsense Reasoning (2003 AAAI Symposium), pp. 27-35, AAAI P ess (2003).
4. J. Bo ego-D´ıaz and A. M. Ch´a ez-Gonz´alez, Managemen Undefinabili y in Da a
Th ough Au oma ed On ology Ex ensions, submi ed (2005).
5. A. Ch´a ez-Gonz´alez, Me eo opological Au oma ed Reasoning o On ology Clean-
ing, o hcoming Ph.D. hesis.
6. A. G. Cohn, B. Benne , J. M. Gooday and N. M. Go s. Rep esen ing and Reasoning
wi h Quali a i e Spa ial Rela ions abou Regions. Chap e 4 in O. S ock (ed.),
Spa ial and Tempo al Reasoning, Kluwe , Do d ec h (1997).
7. A.G. Cohn and N.M. Go s, The ’Egg-Yolk’ Rep esen a ion o Regions wi h In-
de e mina e Bounda ies in P. Bu ough and A. M. F ank (eds), P oc. GISDATA
Specialis Mee ing on Geog aphical Objec s wi h Unde e mined Bounda ies, GIS-
DATA Se ies, ol. 3, Taylo and F ancis, pp. 171-187 (1996).
8. G. S umme, R. Taouil, Y. Bas ide, N. Pasquie and L. Lakhal, Compu ing Icebe g
Concep La ices wi h TITANIC. Da a Knowl. Eng. 42(2) pp. 189-222 (2002).