description logics - dl, alc

Description logics
• Formalisms for expressing concepts, their attributes (or
associated roles), and the relationships between them.
• Can be regarded as providing a KR system based on a
structured representation of knowledge.

Description Logic: (p138) - Ch 9
Three types of non-logical symbols:
• atomic concepts:
Dog, Teenager, GraduateStudent
We include a distinguished concept: Thing
• roles: (all are atomic)
:Age, :Parent, :AreaOfStudy
• constants:
johnSmith, chair128
Four types of logical symbols:
• punctuation: [, ], (, )
• positive integers: 1, 2, 3, ...
• concept-forming operators: ALL, EXISTS, FILLS, AND
• connectives: =, =, and →

[AND Company
For example: [EXISTS 7 :Director]
[ALL :Manager [AND Woman
“a company with at least 7 directors,
whose managers are all women with [FILLS :Degree phD]]]
PhDs, and whose min salary is $24/hr” [FILLS :MinSalary $24.00/hour]]

([AND Surgeon Female] = Doctor) is not valid.

C= is subsumed-by

But it is entailed by a KB that contains
(Surgeon = [AND Specialist [FILLS :Specialty surgery]])
(Specialist C= Doctor)

computing subsumption, that is, determining
whether or not KB = (d subsumed-by e) - 'no negation of alpha query)
assumptions:
- KB is acyclic
- d is atomic, only appears once in LHS
- replace
Under these assumptions, it is sufficient to do the following:
• normalization: using the definitions in the KB, put d and e into a special
normal form, d′ and e′
• structure matching: determine if each part of e′ is matched by a part of d′.
- In other words, for every part of the more general concept,
there must be a corresponding part in the more specific one.
p153. [and person [fills :age 27]

computing satisfaction: To determine if KB = (c → e), we use the following procedure:
1. find the most specific concept d such that KB = (c → d)
2. determine whether or not KB = (d C= e), as before.
joe->person , canCorp, joe is manager of cancorp, manager of cancorp is canadian, so you get joe->canadian

computing classification:
- Positioning a new atom in a taxonomy is called classification
- wine example, Wine is at the top root node, then there's white-very-dry-bordeaux-wine

The Logic ALC
Main components:
• Concepts: classes of individuals
• Roles: binary relations between individuals
• Complex concepts using constructors
• Define terminology: TBox
• Give assertions: ABox
Examples:
• Concept names: Person, Female
• Role names: ParentOf, HasHusband
• Individual names: John, Mary

Assertion C(a) (in B&L it's a->C)

MotherWithoutDaughter = Mother ∀ParentOf.¬Female
(P erson M ale)(John)

A Tableaux Algorithm for ALC (Attributive Concept Language with Complements, more expressive DLs)
• Try to prove concept satisfiability by constructing a model.
• A tableau is a graph representing such a model.
• A set of tableaux expansion rules is used to construct the tableau.
• Either a model is constructed or there is an obvious contradiction.
• If tree T contains a clash the concept C is unsatisfiable.

Unfolded: expand every concept name occurring in C