Part 6: Description Logics: Part 6: Description Logics
Languages for Ontologies: Languages for Ontologies In early days of Artificial Intelligence, ontologies were represented resorting to non-logic-based formalisms
Frames systems and semantic networks
Graphical representation
arguably ease to design
but difficult to manage with complex pictures
formal semantics, allowing for reasoning was missing
Semantic Networks: Semantic Networks Nodes representing concepts (i.e. sets of classes of individual objects)
Links representing relationships
IS_A relationship
More complex relationships may have nodes Person Female Parent Woman Mother hasChild
(1,NIL)
Logics for Semantic Networks: Logics for Semantic Networks Logics was used to describe the semantics of core features of these networks
Relying on unary predicates for describing sets of individuals and binary predicates for relationship between individuals
Typical reasoning used in structure-based representation does not require the full power of 1st order theorem provers
Specialized reasoning techniques can be applied
From Frames to Description Logics: From Frames to Description Logics Logical specialized languages for describing ontologies
The name changed over time
Terminological systems emphasizing that the language is used to define a terminology
Concept languages emphasizing the concept-forming constructs of the languages
Description Logics moving attention to the properties, including decidability, complexity, expressivity, of the languages
Description Logic ALC: Description Logic ALC ALC is the smallest propositionally closed Description Logics. Syntax:
Atomic type:
Concept names, which are unary predicates
Role names, which are binary predicates
Constructs
¬C (negation)
C1 ⊓ C2 (conjunction)
C1 ⊔ C2 (disjunction)
R.C (existential restriction)
R.C (universal restriction)
Semantics of ALC: Semantics of ALC Semantics is based on interpretations (DI,.I) where .I maps:
Each concept name A to AI ⊆ DI
I.e. a concept denotes set of individuals from the domain (unary predicates)
Each role name R to AI ⊆ DI x DI
I.e. a role denotes pairs of (binary relationships among) individuals
An interpretation is a model for concept C iff
CI ≠ {}
Semantics can also be given by translating to 1st order logics
Negation, conjunction, disjunction: Negation, conjunction, disjunction ¬C denotes the set of all individuals in the domain that do not belong to C. Formally
(¬C)I = DI – CI
{x: ¬C(x)}
C1 ⊔ C2 (resp. C1 ⊓ C2) is the set of all individual that either belong to C1 or (resp. and) to C2
(C1 ⊔ C2)I = C1I ⋃ C2I resp. (C1 ⊓ C2)I = C1I ⋂ C2I
{x: C1(x) ⌵ C2(x)} resp. {x: C1(x) C2(x)}
Persons that are not female
Person ⊓ ¬Female
Male or Female individuals
Male ⊔ Female
Quantified role restrictions: Quantified role restrictions Quantifiers are meant to characterize relationship between concepts
R.C denotes the set of all individual which relate via R with at least one individual in concept C
(R.C)I = {d ∈ DI | (d,e) ∈ RI and e ∈ CI}
{x | y R(x,y) C(Y)}
Persons that have a female child
Person ⊓ hasChild.Female
Quantified role restrictions (cont): Quantified role restrictions (cont) R.C denotes the set of all individual for which all individual to which it relates via R belong to concept C
(R.C)I = {d ∈ DI | (d,e) ∈ RI implies e ∈ CI}
{x | y R(x,y) C(Y)}
Persons whose all children are Female
Person ⊓ hasChild.Female
The link in the network above
Parents have at least one child that is a person, and there is no upper limit for children
hasChild.Person ⊓ hasChild.Person
Elephant example: Elephant example Elephants that are grey mammal which have a trunck
Mammal ⊓ bodyPart.Trunk ⊓ color.Grey
Elephants that are heavy mammals, except for Dumbo elephants that are light
Mammal ⊓
(weight.heavy ⊔ (Dumbo ⊓ weight.Light)
Reasoning tasks in DL: Reasoning tasks in DL What can we do with an ontology? What does the logical formalism brings more?
Reasoning tasks
Concept satisfiability (is there any model for C?)
Concept subsumption (does C1I ⊆ C2I for all I?)
C1 ⊑ C2
Subsumption is important because from it one can compute a concept hierarchy
Specialized (decidable and efficient) proof techniques exist for ALC, that do not employ the whole power needed for 1st order logics
Based on tableau algorithms
Representing Knowledge with DL: Representing Knowledge with DL A DL Knowledge base is made of
A TBox: Terminological (background) knowledge
Defines concepts.
Eg. Elephant ≐ Mammal ⊓ bodyPart.Trunk
A ABox: Knowledge about individuals, be it concepts or roles
E.g. dumbo: Elephant or
(lisa,dumbo):haschild
Similar to eg. Databases, where there exists a schema and an instance of a database.
General TBoxes: General TBoxes T is finite set of equation of the form
C1 ≐ C2
I is a model of T if for all C1 ≐ C2 ∈ T, C1I = C2I
Reasoning:
Satisfiability: Given C and T find whether there is a model both of C and of T?
Subsumption (C1 ⊑T C2): does C1I ⊆ C2I holds for all models of T?
Acyclic TBoxes: Acyclic TBoxes For decidability, TBoxes are often restricted to equations
A ≐ C
where A is a concept name (rather than expression)
Moreover, concept A does not appear in the expression C, nor at the definition of any of the concepts there (i.e. the definition is acyclic)
ABoxes: ABoxes Define a set of individuals, as instances of concepts and roles
It is a finite set of expressions of the form:
a:C
(a,b):R
where both a and b are names of individuals, C is a concept and R a role
I is a model of an ABox if it satisfies all its expressions. It satisfies
a:C iff aI ∈ CI
(a,b):R iff (aI,bI) ∈ RI
Reasoning with TBoxes and ABoxes: Reasoning with TBoxes and ABoxes Given a TBox T (defining concepts) and an ABox A defining individuals
Find whether there is a common model (i.e. find out about consistency)
Find whether a concept is subsumed by another concept C1 ⊑T C2
Find whether an individual belongs to a concept (A,T |= a:C), i.e. whether aI ∈ CI for all models of A and T
Inference under ALC: Inference under ALC Since the semantics of ALC can be defined in terms of 1st order logics, clearly 1st order theorem provers can be used for inference
However, ALC only uses a small subset of 1st order logics
Only unary and binary predicates, with a very limited use of quantifiers and connectives
Inference and algorithms can be much simpler
Tableau Algorithms are used for ALC and mostly other description logics
ALC is also decidable, unlike 1st order logics
More expressive DLs: More expressive DLs The limited use of 1st order logics has its advantages, but some obvious drawbacks: Expressivity is also limited
Some concept definitions are not possible to define in ALC. E.g.
An elephant has exactly 4 legs
(expressing qualified number restrictions)
Every mother has (at least) a child, and every son is the child of a mother
(inverse role definition)
Elephant are animal
(define concepts without giving necessary and sufficient conditions)
Extensions of ALC: Extensions of ALC ALCN extends ALC with unqualified number restrictions
≤n R and ≥n R and =n R
Denotes the individuals which relate via R to at least (resp. at most, exactly) n individuals
Eg. Person ⊓ (≥ 2 hasChild)
Persons with at least two children
The precise meaning is defined by (resp. for ≥ and =)
(≤n R)I = {d ∈ DI | #{(d,e) ∈ RI} ≤ n }
It is possible to define the meaning in terms of 1st order logics, with recourse to equality. E.g.
≥2 R is {x: yz, y ≠ z R(x,y) R(x,z)}
≤2 R is
{x: y,z,w, (R(x,y) R(x,z) R(x,w)) (y=z ⌵ y=w ⌵ z=w)}
Qualified number restriction: Qualified number restriction ALCN can be further extended to include the more expressive qualified number restrictions
(≤n R C) and (≥n R C) and (=n R C)
Denotes the individuals which relate via R to at least (resp. at most, exactly) n individuals of concept C
Eg. Person ⊓ (≥ 2 hasChild Female)
Persons with at least two female children
E.g. Mammal ⊓ (=4 bodypart Leg)
Mammals with 4 legs
The precise meaning is defined by (resp. for ≥ and =)
(≤n R)I = {d ∈ DI | #{(d,e) ∈ RI} ≤ n }
Again, it is possible to define the meaning in terms of 1st order logics, with recourse to equality. E.g.
(≥2 R C) is {x: yz, y ≠ z C(y) C(z) R(x,y) R(x,z)}
Further extensions: Further extensions Inverse relations
R- denotes the inverse of R: R- (x,y) = R(y,x)
One of constructs (nominals)
{a1, …, an}, where as are individuals, denotes one of a1, …, an
Statements of subsumption in TBoxes (rather than only definition)
Role transitivity
Trans(R) denotes the transitivity closure of R
SHOIN is the DL resulting from extending ALC with all the above described extensions
It is the underlying logics for the Semantic Web language OWL-DL
The less expressive language SHIF, without nominal is the basis for OWL-Lite
Example: Example From the w3c wine ontology
Wine ⊑
PotableLiquid ⊓ (=1 hasMaker) hasMaker.Winery)
Wine is a potable liquid with exactly one maker, and the maker must be a winery
hasColor-.Wine ⊑ {“white”, “rose”, “red”}
Wines can be either white, rose or red.
WhiteWine ≐ Wine ⊓ hasColor.{“white”}
White wines are exactly the wines with color white.