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”)
∀ x: singer(x) ⇒ person(x)
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
human ⊑ man ⊔ woman
∀ x: human(x) ⇒ man(x) ∨ woman(x)
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 SHIQ .
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
human ≡ man ⊔ woman
6
Description logic syntax
human
list
man
woman
unionOf
DL is primarily concerned with describing sets of entities:
X ⊓ Y
father ≡ parent ⊓ malePerson
7
Intersection
the class of things that are both X and Y
∀ x: father(x) ⇔ parent(x) ∧ malePerson(x)
father ≡ parent ⊓ malePerson
8
Intersection
the class of things that are both X and Y
This corresponds to the First-Order Formula
X ⊓ Y
DL is primarily concerned with describing sets of entities:
∀ x: father(x) ⇔ parent(x) ∧ malePerson(x)
father ≡ parent ⊓ malePerson
9
Intersection
the class of things that are both X and Y
This corresponds to the First-Order Formula
malePerson
parent
father
X ⊓ Y
DL is primarily concerned with describing sets of entities:
X ⊓ Y
X ⊔ Y
¬ X
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
¬ X
X ⊓ Y
X ⊔ Y
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
∀ R.C
the class of things where all outgoing R -links lead to a C
hasOnlyHappyKids ≡ ∀ hasChild.HappyPerson
12
Universal Restriction
a relation
a class
Elnaz6
Fanpop
hasOnlyHappyKids ≡ ∀ hasChild.HappyPerson
13
Universal Restriction
hasChild
hasChild
HappyPerson
∀ R.C
the class of things where all outgoing R -links lead to a C
a relation
a class
∀ x: hasOnlyHappyKids(x)
⇔ ∀ y: hasChild(x,y) ⇒ happyPerson(y)
hasOnlyHappyKids ≡ ∀ hasChild.HappyPerson
14
Universal Restriction
This corresponds to
∀ R.C
the class of things where all outgoing R -links lead to a C
a relation
a class
the class of things where there exists an outgoing R -link leading to a C
∃ R.C
Fanpop
hasHappyKid ≡ ∃ hasChild.HappyPerson
15
Existential Restriction
hasChild
hasChild
HappyPerson
∀ x: hasHappyKid(x)
⇔ ∃ y: hasChild(x,y) ∧ happyPerson(y)
hasHappyKid ≡ ∃ hasChild.HappyPerson
16
Existential Restriction
This corresponds to
>end
>task
the class of things where there exists an outgoing R -link leading to a C
∃ R.C
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 R -link leading to a C
∃ R.C
∀ R.C
the class of things where all outgoing R -links lead to a C
every X is a Y
X ⊑ Y
singer ⊑ person
18
Concept Inclusions
every X is a Y
X ⊑ Y
singer ⊑ person
∀ x: rocksinger(x) ⇒ singer(x) ∧ rockFan(x)
rocksinger ⊑ singer ⊓ rockFan
19
This corresponds to
Concept Inclusions
every X is a Y
X ⊑ Y
singer ⊑ person
rocksinger ⊑ singer ⊓ rockFan
∀ x: rocksinger(x) ⇒ singer(x) ∧ rockFan(x)
happySinger ⊑ singer ⊓ ∀ hasChild.Happy
20
This corresponds to
Concept Inclusions
>end
x and y stand in relationship R
hasChild(elvis, lisa)
R(x,y)
x is an instance of class C
C(x)
Singer(elvis)
HappySinger ≡ Singer ⊓ ∀ hasChild.Happy
HappySinger(elvis)
21
Concept and Role Assertions
>end
>task
Class constructors:
X ⊓ Y
X ⊔ Y
¬ X
∀ R.C
∃ R.C
Assertions:
X ⊑ Y
X ≡ Y
C(x)
R(x, y)
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 n outgoing R links to a C
the class of those things that have at most n outgoing R links to a C
≥ n R.C
≤ n R.C
singer ⊓ ≥ 10 hasChild.Happy
23
Cardinality restrictions
Singers with more than 10 happy children
Singers with exactly 10 happy children:
>end
the class of a, b, and c
{a, b, c}
∃ marriedTo.{priscilla}
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
⊤ ⊑ ∀ hasChild.Happy
∀ hasChild.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”
∃ hasChild.Female
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”
≥ 2 hasChild
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”
≥ 2 hasChild
∀ hasChild.Female
X ⊓ Y
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”
elvis: ∀ hasChild.Female
29
What DL can say
∀ hasChild.Female
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?
singer ⊑ person
dog ⊑ ¬ person
dog(bello)
31
Reasoning tasks
Classical reasoning tasks in DL are:
• Is the knowledge base consistent?
singer ⊑ person
dog ⊑ ¬ person
dog(bello)
person(bello)
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?)
∃ hasChild.{lisa} ⊑ singer ?
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?)
∃ hasChild.{lisa} ⊑ singer ?
leftClass ≡ ∃ hasChild.{Lisa}
notRightClass ≡ ¬ singer
leftClass(bob)
notRightClass(bob)
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?)
∃ hasChild.{lisa} ⊑ singer ?
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.
leftClass ≡ ∃ hasChild.{Lisa}
notRightClass ≡ ¬ singer
leftClass(bob)
notRightClass(bob)
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?)
singer(elvis) ?
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?)
notSinger ≡ ¬ singer
notSinger(elvis)
singer(elvis) ?
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.
notSinger ≡ ¬ singer
notSinger(elvis)
singer(elvis) ?
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?
elvis: singer ⊓ ∃ sings.GoodSong ?
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?
elvis: singer ⊓ ∃ sings.GoodSong ?
notGoodSinger ≡ ¬ (singer ⊓ ∃ sings.GoodSong)
notGoodSinger(elvis)
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
∀ hasChild.Female
41
DL Summary