Transcript PPT - LSDIS
More on Description Logic(s)
Frederick Maier
Note Added 10/27/03
So, there are a few errors that will be obvious to some:
Some of the symbols used in expressions are not in the right font (or
even of the right type in some cases).
Instance checking is not reducible to subsumption in every case (e.g.,
see this).
(The) typical means of proof is based upon satisfiability (as the slides
on semantic tableaux indicate); I should have pointed this out more
explicitly.
Again, most of the material is taken form Enrico Franconi’s course
website (I believe he’s even the originator of the DL logo) .
I’d like to take the presentation down, as it really offers nothing that couldn’t be
found elsewhere just as readily, but I’ll wait until the end of the term.
Overview
The language basics
Interpretations
A Family of Languages
Subsumption
And other problems
Complexity
Assumption:
We
must understand the Syntax,
Semantics, and Inference Mechanisms
of these languages if we are to use
them effectively.
OWL
The language in which our ontologies are
going to be written in is likely going to be
OWL, or something like it.
And OWL is based in part on DL.
What are DL’s?
Key features:
They are a family of Knowledge
Representation languages with a formal
semantics based largely on FOL.
They attempt to discover “implicitly
represented knowledge” using efficient
inference mechanisms.
The complexity of the inferences is an
area of determined research.
Basic Concepts of a DL
Individuals (such as john and mary)
Concepts (such as Man and Woman).
Roles (such as hasChild).
Basic Concepts of a DL
Individuals are treated exactly the same as
constants in FOL.
Concepts are exactly the same as Unary
Predicates in FOL.
Roles are exactly the same as Binary Predicates
in FOL.
Descriptions
Just Like in FOL, what we are dealing with
(ultimately) are sets of individuals and
relations between individuals.
The basic unit of semantic significance is
the Description.
“We are describing sets of individuals”
Defining Descriptions (ALC, a typical language)
A description C or D can be:
A
T
C
C1 ∏ D1
C1 D1
R.C
R.C
an atomic concept.
(top) the universal concept.
(bottom) the null concept
a negated concept
the intersection of concepts.
the union of two concepts.
(restriction)
(existential quantification).
*
*
*
*
*
*
*
[* present in AL. Only atomic concepts can be negated. restricted to R.T]
Interpretations and Models
Mostly, the formal semantics of a DL
follows FOL:
An individual is interpreted as an element
from the universe of discourse.
A concept is interpreted as the set of
elements from the universe to which the
concept applies.
and
and deserve special attention.
Note that they only can come before a Role:
HasChild.Girl
isEmployedBy.Farmer
Remember, they describe sets of individuals.
and
HasChild.Girl would be interpreted as:
The set { x | (y)( HasChild(x,y) Girl(y) ) }
[Note the conditional: Am I in that set?].
and
isEmployedBy.Farmer would be:
The set { x | (y)( isEmployedBy(x,y) & Farmer(y) ) }
A family of languages
The expressiveness of a description logic is
determined by the operators that it uses.
Add or Eliminate certain operators (e.g., , ),
and the statements that can be expressed are
increased/reduced in number.
Higher expressiveness implies higher complexity.
The Language AL
A description C or D can be:
A
T
C
C1 ∏ D1
R.C
R.T
an atomic concept.
(top) the universal concept.
(bottom) the null concept
a negated Atomic concept
the intersection of concepts.
(restriction)
(Limited existential quantification).
A family of languages
Operation
Notation
Union (U)
CB
Complementation (C)
C (Any Concept)
Full Existential Quantification (E)
R.C
Cardinality (N)
≥ nR, ≤nR
Qualified Cardinality (Q)
≥ nR.C, ≤nR.C
Enumeration (O)
{a,b,…}
Selection (F)
f:C
Axioms
We may assign names to complex
descriptions:
Bachelor ≡ Unmarried ∏ Male
Or assert that one concept is subsumed
by another:
CD
These are Axioms of the system.
Subsumption
A concept C subsumes a concept D iff
I(D) I(C)
on every interpretation I. This means the
same as the assertion:
(x)(D(x) C(x)) where
D and C are complex statements
The Subsumption Problem
CD
?
Determining whether one concept logically
contains another is called the subsumption
problem.
Other Problems:
Satisfiability of a Concept or KB {C, C}
Instance Checking Father(john)?
Equivalence CreatureWithHeart ≡ CreatureWithKidney
Disjointness
C∏D
Retrieval
Father(X)? X = {john, robert}
Realization
X(john)?
X = {Father}
Reduction
These problems can be reduced to
subsumption (for languages with
negation).
They can be reduced to the satisfiability
problem, as well.
Complexity
The Subsumption Problem:
It’s undecidable for reasonably expressive
languages,
It’s non-polynomial for fairly restricted
languages.
Complexity
Language
Subsumption
Instance Checking
FLAL
ALE
ALC
P
P
NP
PSPACE
P
P
PSPACE
PSPACE
ALCO
SHIQ
KL-ONE
PSPACE
EXPTIME
undecidable
PSPACE
EXPTIME
undecidable
OWL-Lite
?
?
Inference Mechanisms
ALC is equivalent to L2 and so,
theoretically, we could translate all the
expressions of the DL into L2 and then use
resolution or some algorithm as a decision
procedure.
However, it is generally the case that
Tableau algorithms are computationally
less expensive.
Tableau algorithms
They work by systematically building up a
tree of possible models to for a KB.
If every branch of the tree possesses a
contradiction, then the KB is unsatisfiable.
Tableau proofs are sound and complete for
many languages, including ALC.
Complexity: Notes
In complexity theory the class PSPACE is the set of
decision problems that can be solved by a Turing
machine using a polynomial amount of memory, and
unlimited time.
In complexity theory, EXPTIME is the set of all decision
problems solvable by a deterministic Turing machine in
O(2p(n)) time, where p(n) is a polynomial function of n.
EXPTIME is known to be a subset of EXPSPACE and a
superset of PSPACE, NP-complete, NP, and P. That is
significant because it is currently unknown which (if any)
of those four sets are equal to each other. It is known
however that P is a strict subset of EXPTIME
[From www.wikipedia.org]
References
The Description Logic Website:
http://dl.kr.org/
Presentations from Enrico Franconi’s DL course*:
http://www.inf.unibz.it/~franconi/dl/course/
Chapter 2 of the Description Logic Handbook:
http://www.inf.unibz.it/~franconi/dl/course/dlhb/dlhb-02.pdf
*Upon which this presentation is mostly based.