Transcript Description Logic

Description Logic – 2
1
CS6795 Semantic Web Techniques
4-Nov-05
History
Description Logic Handbook Chapter 1
 Early knowledge representation work from 60’s
–
–
–
–

Led to object oriented programming ideas
–
–

CommonLisp Object System (CLOS)
SmallTalk, C++, Java
Networks of knowledge
–
–
2
Representing classes of objects
Abstraction Hierarchy
Properties of those objects
Constraints on the properties
Semantic Networks (Quillian 1967)
Frames (Minsky 1981)
CS6795 Semantic Web Techniques
4-Nov-05
Example of Network KR


Person, Female, etc are
concepts
hasChild is a property of
Person
–
–

Large arrows are “IS-A” links
–
3
hasChild relates Parent to
Person
Nil means infinity. A Parent
is a Person with between 1
and infinity children
A Mother is a (specialization
of a) Parent
CS6795 Semantic Web Techniques
4-Nov-05
Networks and Logic systems were defined

First order logic can express most of the network
–
–
–
Predicates can be arity 1 or 2 (unary and binary)
Rules can be used for inheritance and some constraints
Mother ISA Parent
X Mother(X) Parent(X)
–
All children of Parents are Persons
X,Y Parent(X)  hasChild(X, Y)  Person(Y)
–
Expect some inferences to be made


Inheritance: All properties of a superclass should also be
properties of its subclass
So all children of Mothers should be Persons
X,Y Mother(X)  hasChild(X, Y)  Person(Y)
4
CS6795 Semantic Web Techniques
4-Nov-05
Network and Logic Systems have
advantages/disadvantages


Networks considered more appealing and more
practical than Logic
Some Network “reasoners” were ad hoc
–

Logic engines all produce the same conclusions
–

Different reasoners give different results
Clearly defined semantics
Logic engines at the time were very general
–
–
Not much known about special reasoners for these
formulas
General resolution-based theorem provers used

5
Generality meant reasoning procedures had high
complexity
CS6795 Semantic Web Techniques
4-Nov-05
Description Logic systems

Brachman and Levesque [1984] “there is a tradeoff between
the expressiveness of a representation language and the
difficulty of reasoning over the representations built using
that language.
–

Schmidt-Schauss and Smolka [1991 ] specialized classical
settings for deductive reasoning to the DL subsets of firstorder logics,
–

–
–
6
Using tableau calculus
Best of both worlds
–

The more expressive the language, the harder the reasoning.
Unary predicates for names of classes
Binary predicates for properties
Conclusions based on inheritance
Derived from Logic but driven by an understanding of how
much reasoning power is needed.
CS6795 Semantic Web Techniques
4-Nov-05
Description Logic
This lecture from DL Handbook Chapter 2
 Description Logics
overcome the ambiguities of early semantic networks
and frames
– first realized in the system KL-One [Brachman and
Schmolze, 1985]
Well-studied and decidable (most DL languages)
Tight coupling between theory and practice
–


7
CS6795 Semantic Web Techniques
4-Nov-05
TBox and ABox
–
TBox: terminology

the vocabulary of an application domain:
–
Concepts: sets of individuals
– Roles: binary relationships between individuals.

Examples:
–
Concepts: Person, Female, Mother
– Role: hasChild, meaning that some person is the child of some other
–
ABox: assertions


about named individuals in terms of this vocabulary
Example
–
Elizabeth and Charles are Persons. We write this as
Person(Elizabeth), and Person(Charles).
– Individuals, like “myCar”, have attributes, like “color”, and those
attributes have values, like “red”. When this happens we say that red
is the colorOf attribute of myCar.
We write this as colorOf(myCar, red).
8
CS6795 Semantic Web Techniques
4-Nov-05
Architecture of a DL System
9
CS6795 Semantic Web Techniques
4-Nov-05
Formulas

Building blocks that allow complex descriptions of
concepts and roles.
–
Example (we’ll look at the syntax in more detail soon.)

A Woman is a Female Person
–

A Mother is a Woman and she has a child
–

10
Woman = Person u Female
Mother = Woman u 9 hasChild.T
The TBox can be used to assign names to
complex descriptions.
We will use the terms description and concept
interchangably.
CS6795 Semantic Web Techniques
4-Nov-05
Reasoning Tasks

TBox reasoning: Determine
–
–
whether a description is satisfiable (i.e., non-contradictory)
whether description A is more general than description B

–

With Subsumption tests one can organize the concepts of a
terminology into a hierarchy according to their generality.
ABox reasoning: Determine
–
–
–
whether its set of assertions is consistent,
whether a particular individual is an instance of a given concept
description.
A concept description can be a query, describing a set of objects


11
A subsumes B if every individual of concept B is also of concept A
With instance tests one can retrieve the individuals that satisfy the query.
We will focus on the reasoning problem of TBox satisifiability
CS6795 Semantic Web Techniques
4-Nov-05
Model Theory

12
Statements in the TBox and in the ABox can be
identified with formulae in first-order logic and the
logical semantics is defined by those formulas
CS6795 Semantic Web Techniques
4-Nov-05
Wrapping your mind around model theory

Recall that a model provides a set of domain elements and a way
to interpret each piece of syntax.
–

Example
–
–

13
We don’t always have a specific world in mind
When a set of formulas is true in some world we say that the
formulas are a model of that world.
–

you can interpret Father(Bruce) and hasChild(Bruce, Mary) when I tell
you who Bruce is and who Mary is and what Father means (a set of
individuals) and what hasChild means (a role, a binary relation)
Whether or not the statements are true depends on whether Bruce is
a Father and on whether Bruce’s child is Mary in the world.
In model theory the weird thing we do is fix the formulas and let
the interpretations vary.
–

It just tells you what is meant by what you wrote down.
They say something accurate about it, but don’t tell you everything.
What makes this useful is that when you do some syntactic
manipulation to generate new formulas from the model, we expect
that the new thing we found is also true in the world
CS6795 Semantic Web Techniques
4-Nov-05
DL Semantics

Defined by standard Tarski-style interpretations:
I = (DI, ¢I), where
–
–
14
DI is the domain (a non-empty set)
¢I is an interpretation function that maps:

Concept (class) name A ! subset AI of DI

Role (property) name R ! binary relation RI over DI

Individual name i ! iI element of DI
CS6795 Semantic Web Techniques
4-Nov-05
The Basic Description Language AL
>I
Negation can only
Semantic
be applied to atomic
concepts
DI (universal concept)
?I
; (bottom concept)
(: A)I
DI \ AI (atomic negation)
(C u D)I
CI u DI (intersection)
(8 R.C)I
{a 2 DI | 8 b.(a,b) 2 RI ! b 2 CI} (value restriction)
(9 R.>)I
{a 2 DI | 9 b.(a,b) 2 RI} (limited exists quantification)
R
RI µ DI £ DI (R is an atomic role)
A
AI µ DI (A is an atomic concept)
Syntax
Only the top concept is
allowed in the scope of an
existential quantification
over a role
The sublanguage FL is obtained by disallowing atomic negation; and
¡
FL0 is obtained by disallowing limited existential quantification.
In predicate logic, concept C can be translated into , C(x) with a free variable x.
15
,8hasChild.Female(x) = 8y.hasChild(x,y) ! Female(y)
CS6795 Semantic Web Techniques
4-Nov-05
What does 8 R.C and 9 R.C mean?

A DogLover is someone whose pets
are all dogs, in this case {C}
DogLover = 8 hasPet.Dog
{p | 8 a, (p, a) 2 hasPet ! a 2 Dog}
Also writen more simply as
{p | hasPet(p, a) ! Dog(a) }

A DogLiker is someone who owns a
dog , in this case {A, C}
DogLiker = 9 hasPet.Dog
{p | hasPet(p, a) Æ Dog(a) }
hasPet
A
Fido
A
Fluffy
B
Tabby
C
Rover
C
Flip
Cat
Fluffy
Tabby
Dog
Fido
Rover
Flip
16
CS6795 Semantic Web Techniques
4-Nov-05
The Family of AL-Languages


AL[U][E][N][C]
U - union
–

E - full existential quantification
–

(C t D) I = CI [ DI
(9 R.C)I ={a 2 DI | 9 b.(a,b) 2 RI Æ b 2 CI}
N - number restrictions
–
at least: (> n R)I ={a 2 DI | |{ b|(a,b)2RI }| > n }
at most: (6 n R)I ={a 2 DI | |{ b|(a,b)2RI }| 6 n }
Person u (6 1 hasChild t (> 3 hasChild u 9 hasChild.Female))
denotes those persons that have either not more than one child or at
least three children, one of which is female.
–

C - full negation
–
17
: CI = DI \ CI
CS6795 Semantic Web Techniques
4-Nov-05
DL as Fragments of Predicate Logic







18
Any concept D is unary predicate with one free variable
Any role R is a primitive binary predicate
9 R.C corresponds to 9 y.R(x,y) Æ C(y)
8 R.C corresponds to 8 y.R(x,y) => C(y)
≥ nR corresponds to
9 y1,...,yn. R(x,y1) Æ... Æ R(x,yn) Æ 8 i<j. yi≠yj
≤ nR corresponds to
8 y1,...,yn+1. R(x, y1) Æ... Æ R(x,yn+1) => 9 i<j. yi=yj
Last two examples demonstrate advantage of variable
free syntax
CS6795 Semantic Web Techniques
4-Nov-05
Knowledge Base in DL

A knowledge base K = hT , Ai comprises two
components:
–
–

The vocabulary consists of concepts and
roles
–
–
19
TBOX T introduces terminology (vocabulary of an
application domain)
ABOX A contains assertions about named
individuals in terms of this vocabulary
concepts denote sets of individuals
roles denote binary relationships between
individuals
CS6795 Semantic Web Techniques
4-Nov-05
TBox and ABox

T (TBox) is a set of axioms of the form:
C v D (concept inclusion)
C ´ D (concept equivalence)
R v S (role inclusion)
has_parent v has_ancestor
R ´ S (role equivalence)
R +v R (role transitivity)
has_mother +v has_ancestor
8has_ancestor.human applies to all successors of has_ancestor

A (ABox) is a set of axioms of the form
x 2 D (concept instantiation)
hx, yi 2 R (role instantiation)
20
CS6795 Semantic Web Techniques
4-Nov-05
An Example about Family Relationships
value restriction(v/r):
(1, NIL)
a role defines a
property of Parent:
hasChild.Person
“IS-A” relationship
defines a hierarchy
over concepts
Examples in TBox:
Woman ´ Person u Female
Examples in ABox:
These are concepts
Mother ´ Woman u 9 hasChild.Person
21
CS6795 Semantic Web Techniques
hasChild(MARY, PETER)
Father(PETER)
4-Nov-05
Name Symbols vs. Base Symbols


atomic concepts occurring in a TBox T can be divided
into two sets, name symbols NT (or defined
concepts) and base symbols BT (or primitive
concepts, occur only on the right-hand side)
a base interpretation for T only interprets the base
symbols.
Base symbols
Name Symbol
22
CS6795 Semantic Web Techniques
4-Nov-05
Unfolding Name Symbols

23
An acyclic TBox can be unfolded or expanded by
eliminating all defined name symbols from the righthand-side with only base symbols:
CS6795 Semantic Web Techniques
4-Nov-05
Reasoning Services


Satisfiability: whether the assertions in an TBox and
ABox has a model
Subsumption: whether one description is more general
than another one
subsumes(C,D)  : sat (: C u D)

Equivalence: whether two classes denote same set
equiv(C,D)  subsumes(C, D) Æ subsumes(D, C)


Instantiation: check if an individual is an instance of
class C
Retrieval: retrieve a set of individuals that instantiate C
 Problems all reducible to satisfiability.
24
CS6795 Semantic Web Techniques
4-Nov-05
Concept Satisfiability

The concepts woman, mother, parent are satisfiable
how about :woman u mother?

The conjunct :woman u mother can never be satisfied

25
CS6795 Semantic Web Techniques
4-Nov-05
ABox Satisfiability

All other inference services can be reduced to
asat(A) where A is the axioms in TBox and ABox
–
instance checking:
instance?(a, C, A) ´ :asat (A [ {a: :C})
–
concept satisfiability:
sat(C) ´ asat{a:C}
–
concept subsumption:
subsumes(C, D) ´ :sat(:CuD) ´ :asat({a::CuD})

Open world assumption
–
–
26
A = {andrew:male, (charles, andrew): has_child}
Does instance?(charles, 8has_child.male, A) hold?
CS6795 Semantic Web Techniques
4-Nov-05
Open World Assumption




Can we prove that instance?(charles, 8has_child.male, A)
holds?
No!
Although the ABox contains only knowledge about one
male child, it is always assumed that represented
information is incomplete.
To make this statement hold, we could add:
–
–
27
charles:8has_child.male or
assert that information about a 2nd child will not be added in
the future: charles: 9 6 1has_child (not possible in ALC as we
need number restrictions)
CS6795 Semantic Web Techniques
4-Nov-05
Reasoner: The Tableau Algorithm



contains a set of completion rules operating on
constraint sets or tableaux
clash triggers
proof procedure:
–
–
–
28
transform unfold the TBox
Transform all concepts into negation normal form (i.e.
negation only occurs only in front of concept names):
 : (C u D) ! :C t :D
 : 9R.C ! 8 R.:C
apply completion rules in arbitrary order as long as
possible
 stops when a clash is found
 terminates if no completion rule is applicable
anymore
 satisfiable iff a clash-free tableau can be derived
CS6795 Semantic Web Techniques
4-Nov-05
Completion Rules for the Logic ALC
Clash Trigger
Role Exists Restriction Rule
{a: A, a: : A} µ A
if 1. a: 9R.C 2 A, and
Conjunction Rule
if 1. a: C u D 2 A, and
2. {a:C, a:D} * A
2. :9b 2 O: {(a,b):R, b:C} µ A
then A’= A [ {(a,b):R, b:C} with b
fresh in A
then A’= A [ {a:C, a:D}
Role Value Restriction Rule
Disjunction Rule
if 1. a: C t D 2 A, and
2. {a:C, a:D} Å A = ?
then A’= A [ {a:C} or
if 1. a: 8 R.C 2 A, and
2. 9b 2 O: (a,b):R 2 A and
3. {b:C} A
then A’= A [ {b:C}
A’= A [ {a:D}
29
CS6795 Semantic Web Techniques
4-Nov-05
Proof for Concept Satisfiability



Does the concept woman subsume mother?
Is the concept :woman u mother unsatisfiable?
Application of completion rules:
:woman u mother is unsatisfiable
) the concept woman subsumes the concept mother

30
CS6795 Semantic Web Techniques
4-Nov-05
DL for the Semantic Web

Web Ontology Language (OWL): W3C Recommendation on 10
Feb 2004

builds on RDF and RDF Schema and adds more vocabulary for
describing properties and classesExtends existing Web
standards

has three increasingly-expressive sublanguages: OWL Lite
(based on DL SHIF (D)) , OWL DL (based on DL SHOIN(D)),
and OWL Full (OWL DL + RDF)
benefits from many years of DL research

–
–
–
–
–
31
Well defined semantics
Formal properties well understood (complexity, decidability)
Known reasoning algorithms
Implemented systems (highly optimised)
Example: Ontology of Books
CS6795 Semantic Web Techniques
4-Nov-05
OWL Class Constructor
32
CS6795 Semantic Web Techniques
4-Nov-05
OWL Axioms

Axioms (mostly) reducible to inclusion (v)
–
33
e.g. C ´ D iff both C v D and D v C
CS6795 Semantic Web Techniques
4-Nov-05
Concrete Abstract Syntax


Easier to read than OWL, much closer to logic
ALCAS.pl
–
–
Prolog implementation of ALC reasoner using CAS
Currently only does TBox consistency

–
–
34
Working on this…
Shows actions at various steps.
See http://owl.man.ac.uk/2003/concrete/latest/
CS6795 Semantic Web Techniques
4-Nov-05