Description Logics
CC-BY
Fabian M. Suchanek
A
knowledge base
is a computer-processable collection of knowledge about the world.
2
Def: Knowledge Base
Singer
type
died
?
born
1935
An
ontology language
is a formal language used to describe and reason on knowledge bases.
For example: First Order Logic (“FOL”)
∀ ｘ： ｓｉｎｇｅｒ（ｘ） ⇒ ｐｅｒｓｏｎ（ｘ）
Problem: First Order Logic is undecidable!
3
Def: Ontology language
->decidability
A
description logic
(DL) is a special logic, which
•
is a subset of FOL
•
uses only unary and binary predicates (relations)
•
is decidable
•
comes with a special syntax that does not use variables
ｈｕｍａｎ ⊑ ｍａｎ ⊔ ｗｏｍａｎ
∀ ｘ： ｈｕｍａｎ（ｘ） ⇒ ｍａｎ（ｘ） ∨ ｗｏｍａｎ（ｘ）
4
Def: Description logic
Example:
DL formula
Equivalent FOL formula
>SHIQ
There are several description logics. They allow or disallow, for example,
•
union of concepts (“U”)
•
functional predicates (“F”)
•
complex concept negation (“C”)
•
cardinality restrictions (“N”)
This yields abbreviations for these logics, such as ＳＨＩＱ .
We will look at
, which is the basis of OWL 2, the language used on the Semantic Web.
5
Description logics
Different syntaxes have been developed to say the same thing in OWL:
<human> owl:unionOf <list>
<list> rdf:_1 <man>
<list> rdf:_2 <man>
ObjectUnionOf(man woman)
Class: Human
EquivalentTo: Man or Woman
We will stick to this one
ｈｕｍａｎ ≡ ｍａｎ ⊔ ｗｏｍａｎ
6
Description logic syntax
human
list
man
woman
unionOf
DL is primarily concerned with describing sets of entities:
Ｘ ⊓ Ｙ
ｆａｔｈｅｒ ≡ ｐａｒｅｎｔ ⊓ ｍａｌｅＰｅｒｓｏｎ
7
Intersection
the class of things that are both X and Y
∀ ｘ： ｆａｔｈｅｒ（ｘ） ⇔ ｐａｒｅｎｔ（ｘ） ∧ ｍａｌｅＰｅｒｓｏｎ（ｘ）
ｆａｔｈｅｒ ≡ ｐａｒｅｎｔ ⊓ ｍａｌｅＰｅｒｓｏｎ
8
Intersection
the class of things that are both X and Y
This corresponds to the First-Order Formula
Ｘ ⊓ Ｙ
DL is primarily concerned with describing sets of entities:
∀ ｘ： ｆａｔｈｅｒ（ｘ） ⇔ ｐａｒｅｎｔ（ｘ） ∧ ｍａｌｅＰｅｒｓｏｎ（ｘ）
ｆａｔｈｅｒ ≡ ｐａｒｅｎｔ ⊓ ｍａｌｅＰｅｒｓｏｎ
9
Intersection
the class of things that are both X and Y
This corresponds to the First-Order Formula
malePerson
parent
father
Ｘ ⊓ Ｙ
DL is primarily concerned with describing sets of entities:
Ｘ ⊓ Ｙ
Ｘ ⊔ Ｙ
¬ Ｘ
10
Intersection, Union, Complement
>task
the class of things that are X or Y
the class of things that are both X and Y
the class of things that are not X
person, parent, hardRockSinger, softRockSinger,
happyPerson, marriedPerson, malePerson
rocksinger, unmarried-rock-singing-father,
non-rock-singing-person
¬ Ｘ
Ｘ ⊓ Ｙ
Ｘ ⊔ Ｙ
11
Define
Task: Given these classes
the class of things that are X or Y
the class of things that are both X and Y
the class of things that are not X
Intersection, Union, Complement
∀ Ｒ．Ｃ
the class of things where all outgoing Ｒ -links lead to a Ｃ
ｈａｓＯｎｌｙＨａｐｐｙＫｉｄｓ ≡ ∀ ｈａｓＣｈｉｌｄ．ＨａｐｐｙＰｅｒｓｏｎ
12
Universal Restriction
a relation
a class
Elnaz6
Fanpop
ｈａｓＯｎｌｙＨａｐｐｙＫｉｄｓ ≡ ∀ ｈａｓＣｈｉｌｄ．ＨａｐｐｙＰｅｒｓｏｎ
13
Universal Restriction
hasChild
hasChild
HappyPerson
∀ Ｒ．Ｃ
the class of things where all outgoing Ｒ -links lead to a Ｃ
a relation
a class
∀ ｘ： ｈａｓＯｎｌｙＨａｐｐｙＫｉｄｓ（ｘ）
⇔ ∀ ｙ： ｈａｓＣｈｉｌｄ（ｘ，ｙ） ⇒ ｈａｐｐｙＰｅｒｓｏｎ（ｙ）
ｈａｓＯｎｌｙＨａｐｐｙＫｉｄｓ ≡ ∀ ｈａｓＣｈｉｌｄ．ＨａｐｐｙＰｅｒｓｏｎ
14
Universal Restriction
This corresponds to
∀ Ｒ．Ｃ
the class of things where all outgoing Ｒ -links lead to a Ｃ
a relation
a class
the class of things where there exists an outgoing Ｒ -link leading to a Ｃ
∃ Ｒ．Ｃ
Fanpop
ｈａｓＨａｐｐｙＫｉｄ ≡ ∃ ｈａｓＣｈｉｌｄ．ＨａｐｐｙＰｅｒｓｏｎ
15
Existential Restriction
hasChild
hasChild
HappyPerson
∀ ｘ： ｈａｓＨａｐｐｙＫｉｄ（ｘ）
⇔ ∃ ｙ： ｈａｓＣｈｉｌｄ（ｘ，ｙ） ∧ ｈａｐｐｙＰｅｒｓｏｎ（ｙ）
ｈａｓＨａｐｐｙＫｉｄ ≡ ∃ ｈａｓＣｈｉｌｄ．ＨａｐｐｙＰｅｒｓｏｎ
16
Existential Restriction
This corresponds to
>end
>task
the class of things where there exists an outgoing Ｒ -link leading to a Ｃ
∃ Ｒ．Ｃ
Given:
singer, happyPerson, hasChild
Build:
• the class of singers with only happy children
• the class of happy people who have at least one happy singer as child
17
Task: Restrictions
>end
the class of things where there exists an outgoing Ｒ -link leading to a Ｃ
∃ Ｒ．Ｃ
∀ Ｒ．Ｃ
the class of things where all outgoing Ｒ -links lead to a Ｃ
every X is a Y
Ｘ ⊑ Ｙ
ｓｉｎｇｅｒ ⊑ ｐｅｒｓｏｎ
18
Concept Inclusions
every X is a Y
Ｘ ⊑ Ｙ
ｓｉｎｇｅｒ ⊑ ｐｅｒｓｏｎ
∀ ｘ： ｒｏｃｋｓｉｎｇｅｒ（ｘ） ⇒ ｓｉｎｇｅｒ（ｘ） ∧ ｒｏｃｋＦａｎ（ｘ）
ｒｏｃｋｓｉｎｇｅｒ ⊑ ｓｉｎｇｅｒ ⊓ ｒｏｃｋＦａｎ
19
This corresponds to
Concept Inclusions
every X is a Y
Ｘ ⊑ Ｙ
ｓｉｎｇｅｒ ⊑ ｐｅｒｓｏｎ
ｒｏｃｋｓｉｎｇｅｒ ⊑ ｓｉｎｇｅｒ ⊓ ｒｏｃｋＦａｎ
∀ ｘ： ｒｏｃｋｓｉｎｇｅｒ（ｘ） ⇒ ｓｉｎｇｅｒ（ｘ） ∧ ｒｏｃｋＦａｎ（ｘ）
ｈａｐｐｙＳｉｎｇｅｒ ⊑ ｓｉｎｇｅｒ ⊓ ∀ ｈａｓＣｈｉｌｄ．Ｈａｐｐｙ
20
This corresponds to
Concept Inclusions
>end
ｘ and ｙ stand in relationship Ｒ
ｈａｓＣｈｉｌｄ（ｅｌｖｉｓ， ｌｉｓａ）
Ｒ（ｘ，ｙ）
ｘ is an instance of class Ｃ
Ｃ（ｘ）
Ｓｉｎｇｅｒ（ｅｌｖｉｓ）
ＨａｐｐｙＳｉｎｇｅｒ ≡ Ｓｉｎｇｅｒ ⊓ ∀ ｈａｓＣｈｉｌｄ．Ｈａｐｐｙ
ＨａｐｐｙＳｉｎｇｅｒ（ｅｌｖｉｓ）
21
Concept and Role Assertions
>end
>task
Class constructors:
Ｘ ⊓ Ｙ
Ｘ ⊔ Ｙ
¬ Ｘ
∀ Ｒ．Ｃ
∃ Ｒ．Ｃ
Assertions:
Ｘ ⊑ Ｙ
Ｘ ≡ Ｙ
Ｃ（ｘ）
Ｒ（ｘ， ｙ）
22
Task: Description Logic
Given:
male, person, happyPerson marriedTo, hasChild
Build:
•
the class of married people
•
the class of people married to at least 1 happy person
•
build the class of happy male married people
•
say that married people are happy
>end
the class of those things that have at least ｎ outgoing Ｒ links to a Ｃ
the class of those things that have at most ｎ outgoing Ｒ links to a Ｃ
≥ ｎ Ｒ．Ｃ
≤ ｎ Ｒ．Ｃ
ｓｉｎｇｅｒ ⊓ ≥ １０ ｈａｓＣｈｉｌｄ．Ｈａｐｐｙ
23
Cardinality restrictions
Singers with more than 10 happy children
Singers with exactly 10 happy children:
>end
the class of a, b, and c
｛ａ， ｂ， ｃ｝
∃ ｍａｒｒｉｅｄＴｏ．｛ｐｒｉｓｃｉｌｌａ｝
24
Enumerations
(the class of Priscilla's husbands)
>end
the class of all things (“top”)
the empty class (“bottom”)
⊤
⊥
Examples:
•
People with an unhappy child are not happy.
•
People whose children are all male are not happy
⊤ ⊑ ∀ ｈａｓＣｈｉｌｄ．Ｈａｐｐｙ
∀ ｈａｓＣｈｉｌｄ．Ｈａｐｐｙ ⊑ ⊥
25
Top and Bottom
Everybody has only happy children:
Nobody has only happy children:
>end
DL basically reasons about properties such as
• having a link to an element of a class
“Those who have a female child”
∃ ｈａｓＣｈｉｌｄ．Ｆｅｍａｌｅ
26
What DL can say
DL basically reasons about properties such as
• having a/all links to an element of a class
• having at most or at least n links of a certain type
“Those who have more than 1 child”
≥ ２ ｈａｓＣｈｉｌｄ
27
What DL can say
DL basically reasons about properties such as
• having a/all links to an element of a class
• having at most or at least n links of a certain type
• being in two classes at the same time
“Those that have more than 1 child and have only female children”
≥ ２ ｈａｓＣｈｉｌｄ
∀ ｈａｓＣｈｉｌｄ．Ｆｅｍａｌｅ
Ｘ ⊓ Ｙ
28
What DL can say
DL basically reasons about properties such as
• having a/all links to an element of a class
• having at most or at least n links of a certain type
• being in two classes at the same time
• belonging to such a class
“Elvis has only female children”
ｅｌｖｉｓ： ∀ ｈａｓＣｈｉｌｄ．Ｆｅｍａｌｅ
29
What DL can say
∀ ｈａｓＣｈｉｌｄ．Ｆｅｍａｌｅ
DL basically reasons about properties such as
• having a/all links to an element of a class
• having at most or at least n links of a certain type
• being in two classes at the same time
• belonging to such a class
• standing in a relationship
All of these statements correspond to First Order Logic formulae.
The Entscheidungsproblem is decidable on this subset of FOL!
30
What DL can say
>end
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
ｓｉｎｇｅｒ ⊑ ｐｅｒｓｏｎ
ｄｏｇ ⊑ ¬ ｐｅｒｓｏｎ
ｄｏｇ（ｂｅｌｌｏ）
31
Reasoning tasks
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
ｓｉｎｇｅｒ ⊑ ｐｅｒｓｏｎ
ｄｏｇ ⊑ ¬ ｐｅｒｓｏｎ
ｄｏｇ（ｂｅｌｌｏ）
ｐｅｒｓｏｎ（ｂｅｌｌｏ）
32
Reasoning tasks
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
(Are all parents of Lisa singers?)
∃ ｈａｓＣｈｉｌｄ．｛ｌｉｓａ｝ ⊑ ｓｉｎｇｅｒ ?
33
Reasoning tasks
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
(Are all parents of Lisa singers?)
∃ ｈａｓＣｈｉｌｄ．｛ｌｉｓａ｝ ⊑ ｓｉｎｇｅｒ ?
ｌｅｆｔＣｌａｓｓ ≡ ∃ ｈａｓＣｈｉｌｄ．｛Ｌｉｓａ｝
ｎｏｔＲｉｇｈｔＣｌａｓｓ ≡ ¬ ｓｉｎｇｅｒ
ｌｅｆｔＣｌａｓｓ（ｂｏｂ）
ｎｏｔＲｉｇｈｔＣｌａｓｓ（ｂｏｂ）
34
Reasoning tasks
Can be reduced to the consistency problem:
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
(Are all parents of Lisa singers?)
∃ ｈａｓＣｈｉｌｄ．｛ｌｉｓａ｝ ⊑ ｓｉｎｇｅｒ ?
More precisely, we ask: Does it follow
necessarily from the KB that one class is a
subclass of the other?
If so, we get a contradiction here.
ｌｅｆｔＣｌａｓｓ ≡ ∃ ｈａｓＣｈｉｌｄ．｛Ｌｉｓａ｝
ｎｏｔＲｉｇｈｔＣｌａｓｓ ≡ ¬ ｓｉｎｇｅｒ
ｌｅｆｔＣｌａｓｓ（ｂｏｂ）
ｎｏｔＲｉｇｈｔＣｌａｓｓ（ｂｏｂ）
35
Reasoning tasks
Can be reduced to the consistency problem:
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
• Is an individual an instance of a class?
(Is Elvis a singer?)
ｓｉｎｇｅｒ（ｅｌｖｉｓ） ?
36
Reasoning tasks
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
• Is an individual an instance of a class?
(Is Elvis a singer?)
ｎｏｔＳｉｎｇｅｒ ≡ ¬ ｓｉｎｇｅｒ
ｎｏｔＳｉｎｇｅｒ（ｅｌｖｉｓ）
ｓｉｎｇｅｒ（ｅｌｖｉｓ） ?
37
Reasoning tasks
Can be reduced to the consistency problem:
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
• Is an individual an instance of a class?
(Is Elvis a singer?)
More precisely, we ask: Does it follow necessarily
from the KB that Elvis is a singer?
If so, this assertion will cause a contradiction.
ｎｏｔＳｉｎｇｅｒ ≡ ¬ ｓｉｎｇｅｒ
ｎｏｔＳｉｎｇｅｒ（ｅｌｖｉｓ）
ｓｉｎｇｅｒ（ｅｌｖｉｓ） ?
38
Reasoning tasks
Can be reduced to the consistency problem:
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
• Is an individual an instance of a class?
• Does an individual have a certain property?
ｅｌｖｉｓ： ｓｉｎｇｅｒ ⊓ ∃ ｓｉｎｇｓ．ＧｏｏｄＳｏｎｇ ?
39
Reasoning tasks
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
• Is one class a subclass of another class?
• Is an individual an instance of a class?
• Does an individual have a certain property?
ｅｌｖｉｓ： ｓｉｎｇｅｒ ⊓ ∃ ｓｉｎｇｓ．ＧｏｏｄＳｏｎｇ ?
ｎｏｔＧｏｏｄＳｉｎｇｅｒ ≡ ¬ （ｓｉｎｇｅｒ ⊓ ∃ ｓｉｎｇｓ．ＧｏｏｄＳｏｎｇ）
ｎｏｔＧｏｏｄＳｉｎｇｅｒ（ｅｌｖｉｓ）
40
Reasoning tasks
Can be reduced to the consistency problem:
OWL DL is a decidable subset of First Order Logic.
It allows describing properties of objects in a manner inspired by set theory.
There are a number of free OWL DL reasoners available online:
• Pellet
• FaCT++
• Prova
∀ ｈａｓＣｈｉｌｄ．Ｆｅｍａｌｅ
41
DL Summary