Transcript Ontology Reasoning

Ontology Reasoning
Majid Sazvar
[email protected]
Advisor: Dr. Naghibzadeh
Knowledge Engineering Research Group
Ferdowsi University of Mashhad
2010
Ontology Reasoning - Majid Sazvar - 2010
Outline
•
•
•
•
Introduction
Description Logics
Horn Logic
Ontology Reasoning
–
–
–
•
•
Why do we want it?
How do we do it?
Reasoning Tasks
Overview of DL Reasoners
Current Researches
2
Introduction
Ontology Reasoning - Majid Sazvar - 2010
Introduction
KR + Reasoning = Knowledge Based System
• KR: Providing high-level descriptions of the world that can be
effectively used by computer.
• Reasoning (Knowledge Processing): Finding implicit
consequences from explicitly represented knowledge.
4
Ontology Reasoning - Majid Sazvar - 2010
Knowledge Representation Methods
1. Logic-Based Methods (particularly in the form of predicate
logic  First Order Logic)
2. Non-Logic-Based Methods
–
–
–
Rule-Based
Semantic Networks
Frame-Based
5
Ontology Reasoning - Majid Sazvar - 2010
The Importance of Logic
•
High-level language for expressing knowledge
•
High expressive power
•
Well-understood formal semantics
•
Precise notion of logical consequence
•
Proof systems that can automatically derive statements
syntactically from a set of premises
6
Ontology Reasoning - Majid Sazvar - 2010
The Importance of Logic (2)
•
There exist proof systems for which semantic logical
consequence coincides with syntactic derivation within the
proof system
–
•
Predicate logic is unique in the sense that sound and
complete proof systems do exist.
–
•
Soundness & completeness
Not for more expressive logics (higher-order logics)
Logic can provide explanations for answers
–
By tracing a proof
7
Description Logics
Ontology Reasoning - Majid Sazvar - 2010
Specializations of Predicate Logic: RDF and OWL
• RDF/S and OWL (Lite and DL) are specializations of predicate
logic
– correspond roughly to a description logic
• They define reasonable subsets of logic
• Trade-off between the expressive power and the
computational complexity:
– The more expressive the language, the less efficient the corresponding
proof systems
9
Ontology Reasoning - Majid Sazvar - 2010
What Are Description Logics?
• A family of logic based Knowledge Representation
formalisms
– Descendants of semantic networks
– Describe domain in terms of concepts (classes), roles (properties,
relationships) and individuals
• Distinguished by:
– Decidable fragments of FOL
– Provision of inference services
• Decision procedures for key problems (satisfiability, subsumption,
etc)
• Implemented systems (highly optimised)
10
Ontology Reasoning - Majid Sazvar - 2010
DL Basics
• Concept names are equivalent to unary predicates
– In general, concepts equiv to formulae with one free
variable
• Role names are equivalent to binary predicates
– In general, roles equiv to formulae with two free variables
• Individual names are equivalent to constants
• Operators restricted so that:
– Language is decidable and, if possible, of low complexity
– No need for explicit use of variables
• Restricted form of 9 and 8
• Features such as counting can be succinctly expressed
11
Ontology Reasoning - Majid Sazvar - 2010
DL System Architecture
Man ´ Human u Male
Happy-Father ´ Man u 9 has-child
Female u …
Abox (data)
John : Happy-Father
hJohn, Maryi : has-child
Interface
Tbox (schema)
Inference System
Knowledge Base
John: 6 1 has-child
12
Ontology Reasoning - Majid Sazvar - 2010
The DL Family
• Given DL defined by set of concept and role forming operators
• Smallest propositionally closed DL is ALC
– Concepts constructed using u, t, :, 9 and 8
• S often used for ALC with transitive roles (R+)
• Additional letters indicate other extension, e.g.:
–
–
–
–
–
H for role inclusion axioms (role hierarchy)
O for nominals (singleton classes, written {x})
I for inverse roles
N for number restrictions (of form 6nR, >nR)
Q for qualified number restrictions (of form 6nR.C, >nR.C)
• E.g., ALC + R+ + role hierarchy + inverse roles + QNR = SHIQ
• Have been extended in many directions
13
Ontology Reasoning - Majid Sazvar - 2010
DL Semantics
• Semantics defined by interpretations
• An interpretation I = (DI, ¢I), where
– 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
14
Ontology Reasoning - Majid Sazvar - 2010
DL Semantics (cont.)
• Interpretation function ¢I extends to concept (and role)
expressions in the obvious way, e.g.:
15
Ontology Reasoning - Majid Sazvar - 2010
DL Knowledge Base
• A DL Knowledge base K is a pair hT ,Ai where
– T is a set of “terminological” axioms (the Tbox)
– A is a set of “assertional” axioms (the Abox)
• Tbox axioms are of the form:
C v D, C ´ D, R v S, R ´ S and R+ v R
where C, D concepts, R, S roles, and R+ set of transitive roles
• Abox axioms are of the form:
x:D, hx,yi:R
where x,y are individual names, D a concept and R a role
16
Ontology Reasoning - Majid Sazvar - 2010
Knowledge Base Semantics
• An interpretation I satisfies (models) a Tbox axiom A (I ² A):
I ² C v D iff CI µ DI
I ² R v S iff RI µ SI
I ² R+ v R iff (RI)+ µ RI
I ² C ´ D iff CI = DI
I ² R ´ S iff RI = SI
• I satisfies a Tbox T (I ² T ) iff I satisfies every axiom A in T
• An interpretation I satisfies (models) an Abox axiom A (I ² A):
I ² x:D iff xI 2 DI
I ² hx,yi:R iff (xI,yI) 2 RI
• I satisfies an Abox A (I ² A) iff I satisfies every axiom A in A
• I satisfies an KB K (I ² K) iff I satisfies both T and A
17
Ontology Reasoning - Majid Sazvar - 2010
Short History of Description Logics
Phase 1:
– Incomplete systems (Back, Classic, Loom, . . . )
– Based on structural algorithms
Phase 2:
– Development of tableau algorithms and complexity results
– Investigation of optimisation techniques
Phase 3:
– Tableau algorithms for very expressive DLs
– Highly optimised tableau systems for ExpTime logics (e.g., FaCT, DLP,
Racer)
– Relationship to modal logic and decidable fragments of FOL
18
Ontology Reasoning - Majid Sazvar - 2010
Recent Developments
Phase 4:
– Mainstream applications and tools
• Databases
– Consistency of conceptual schemata (EER, UML etc.)
– Schema integration
– Query subsumption (w.r.t. a conceptual schema)
• Ontologies, e-Science and Semantic Web/Grid
– Ontology engineering (schema design, maintenance, integration)
– Reasoning with ontology-based annotations (data)
– Mature implementations
• Research implementations
– FaCT, FaCT++, Racer, Pellet, …
• Commercial implementations
– Cerebra system from Network Inference (and now Racer)
19
Horn Logic
Ontology Reasoning - Majid Sazvar - 2010
Specializations of Predicate Logic: Horn Logic
• A rule has the form: A1, . . ., An  B
– Ai and B are atomic formulas
• There are 2 ways of reading such a rule:
– Deductive rules: If A1,..., An are known to be true, then B is also true
– Reactive rules: If the conditions A1,..., An are true, then carry out the
action B
21
Ontology Reasoning - Majid Sazvar - 2010
Description Logic vs. Horn Logic
• Neither of them is a subset of the other
• It is impossible to assert that a person X who is brother of Y is
uncle of Z (where Z is child of Y) in OWL
– This can be done easily using rules:
brother(X,Y), childOf(Z,Y)  uncle(X,Z)
• Rules cannot assert the information that a person is either a
man or a woman
– This information is easily expressed in OWL using disjoint union
22
Ontology Reasoning - Majid Sazvar - 2010
Monotonic vs. Non-monotonic Rules
•
Example: An online vendor wants to give a special discount
if it is a customer’s birthday
Solution 1
R1: If birthday, then special discount
R2: If not birthday, then not special discount
–
But what happens if a customer refuses to provide his birthday due
to privacy concerns?
23
Ontology Reasoning - Majid Sazvar - 2010
Monotonic vs. Non-monotonic Rules (2)
Solution 2
R1: If birthday, then special discount
R2’: If birthday is not known, then not special discount
– Solves the problem but:
• The premise of rule R2' is not within the expressive power of predicate logic
• We need a new kind of rule system
24
Ontology Reasoning - Majid Sazvar - 2010
Monotonic vs. Non-monotonic Rules (3)
•
The solution with rules R1 and R2 works in case we have
complete information about the situation
•
The new kind of rule system will find application in cases
where the available information is incomplete
•
R2’ is a nonmonotonic rule
25
Ontology Reasoning - Majid Sazvar - 2010
Example: Family Relations
•
Facts in a database about relations:
–
–
–
–
mother(X,Y), X is the mother of Y
father(X,Y), X is the father of Y
male(X), X is male
female(X), X is female
• Inferred relation parent: A parent is either a father or a
mother
mother(X,Y)  parent(X,Y)
father(X,Y)  parent(X,Y)
26
Ontology Reasoning - Majid Sazvar - 2010
Example: Family Relations (2)
• male(X), parent(P,X), parent(P,Y), notSame(X,Y)
brother(X,Y)
• female(X), parent(P,X), parent(P,Y), notSame(X,Y)
sister(X,Y)
• brother(X,P), parent(P,Y)  uncle(X,Y)
• mother(X,P), parent(P,Y)  grandmother(X,Y)
• parent(X,Y)  ancestor(X,Y)
• ancestor(X,P), parent(P,Y)  ancestor(X,Y)


27
Ontology Reasoning:
Why do We Want It?
Ontology Reasoning - Majid Sazvar - 2010
Why Ontology Reasoning?
•
Given key role of ontologies in many applications, it is essential to provide
tools and services to help users:
– Design and maintain high quality ontologies, e.g.:
•
•
•
•
Meaningful — all named classes can have instances
Correct — captured intuitions of domain experts
Minimally redundant — no unintended synonyms
Richly axiomatised — (sufficiently) detailed descriptions
– Answer queries over ontology classes and instances,
e.g.:
• Find more general/specific classes
• Retrieve individuals/tuples matching a given query
– Integrate and align multiple ontologies
29
Ontology Reasoning - Majid Sazvar - 2010
Why Decidable Reasoning?
• OWL is an W3C standard DL based ontology language
– OWL constructors/axioms restricted so reasoning is decidable
• Consistent with Semantic Web's layered architecture
– XML provides syntax transport layer
– RDF(S) provides basic relational language and simple ontological
primitives
– OWL provides powerful but still decidable ontology language
– Further layers (e.g. SWRL) will extend OWL
• Will almost certainly be undecidable
• W3C requirement for “implementation experience”
– “Practical” decision procedures
– Several implemented systems
– Evidence of empirical tractability
30
Ontology Reasoning - Majid Sazvar - 2010
Why Correct Reasoning?
• Need to have high level of confidence in reasoner
– Most interesting/useful inferences are those that were
unexpected
– Likely to be ignored/dismissed if reasoner known to be unreliable
• Many realistic web applications will be agent ↔ agent
– No human intervention to spot glitches in reasoning
31
Ontology Reasoning:
How do we do it?
Ontology Reasoning - Majid Sazvar - 2010
Use a (Description) Logic
• OWL DL based on SHIQ Description Logic
– In fact it is equivalent to SHOIN(Dn) DL
• OWL DL Benefits from many years of DL research
–
–
–
–
Well defined semantics
Formal properties well understood (complexity, decidability)
Known reasoning algorithms
Implemented systems (highly optimised)
• In fact there are three “species” of OWL (!)
– OWL full is union of OWL syntax and RDF
– OWL DL restricted to First Order fragment (¼ DAML+OIL)
– OWL Lite is “simpler” subset of OWL DL (equiv to SHIF(Dn))
33
Ontology Reasoning - Majid Sazvar - 2010
Class/Concept Constructors
•
C is a concept (class); P is a role (property); x is an individual name
34
Ontology Reasoning - Majid Sazvar - 2010
Ontologies / Knowledge Bases
• OWL ontology equivalent to a DL Knowledge Base
• OWL ontology consists of a set of axioms and facts
– Note: an ontology is usually thought of as containing only Tbox
axioms (schema)---OWL is non-standard in this respect
• Recall that a DL KB K is a pair hT ,Ai where
– T is a set of “terminological” axioms (the Tbox)
– A is a set of “assertional” axioms (the Abox)
35
Ontology Reasoning - Majid Sazvar - 2010
Ontology/Tbox Axioms
• Obvious FO/Modal Logic equivalences
– E.g., DL: C v D
FOL: x.C(x) !D(x)
ML: C!D
• Often distinguish two kinds of Tbox axioms
– “Definitions” C v D or C ´ D where C is a concept name
– General Concept Inclusion axioms (GCIs) where C may be complex
36
Ontology Reasoning - Majid Sazvar - 2010
Ontology Facts / Abox Axioms
• Note: using nominals (e.g., in SHOIN), can
reduce Abox axioms to concept inclusion axioms
–
–
equivalent to
equivalent to
37
Ontology Reasoning:
Reasoning Tasks
Ontology Reasoning - Majid Sazvar - 2010
Reasoning Tasks
• TBOX reasoning tasks
– Satisfiability checks whether a class C can have instances
according to the current ontology.
– Subsumption checks whether a class D subsumes a class C
according to the current ontology. Property subsumption is
defined analogously.
– Classification computing the complete subsumption hierarchy of
the ontology.
39
Ontology Reasoning - Majid Sazvar - 2010
Reasoning Tasks
• ABOX reasoning tasks
– Consistency checks whether the Abox is consistent with respect to
the TBox.
– Instance checking checks whether an assertion is entailed by the
Abox.
– Retrieval problem retrieves all individuals that instantiate a class
C, dually we can find all named classes C that an individual a
belongs to.
– Property fillers retrieves, given a property R and an individual i, all
individuals x which are related with i via R. Similarly we can
retrieve the set of all named properties R between two individuals
i and j, ask whether the pair (i,j) is a filler of P or ask for all pairs
(i,j) that are a filler of P.
40
Ontology Reasoning - Majid Sazvar - 2010
Reasoning Tasks
• ABOX reasoning tasks
– Conjunctive Queries are a popular query formalism capable of
expressing the class of selection/projection/join/renaming
relational queries.
• Theoretically it is possible to reduce all reasoning tasks to
the task of checking KB consistency.
– However in practice this is not necessarily the fastest way of
reasoning and various optimizations are taken for different tasks.
41
Overview of DL Reasoners
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners
• CEL
– is a free (for non-commercial use) LISP-based reasoner for EL+. It
implements a refined version of a known polynomial-time
classification algorithm and supports new features like module
extraction and axiom pinpointing. Currently, it accepts inputs in a
small extension of the KRSS syntax and supports the DIG interface.
• Cerebra Engine
– is a commercial C++-based reasoner. It implements a tableaubased decision procedure for general TBoxes (subsumption,
satisfiability, classification) and ABoxes (retrieval, tree-conjunctive
query answering using a XQuery-like syntax). It supports the OWLAPI and comes with numerous other features.
43
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (2)
• Bossam
– an RETE-based rule engine with native supports for reasoning
over OWL ontologies, SWRL ontologies, and RuleML rules.
• FaCT++
– is a free (GPL/LGPL) open-source C++-based reasoner for SROIQ
with simple datatypes (i.e., for OWL 2). It implements a tableaubased decision procedure for general TBoxes (subsumption,
satisfiability, classification) and ABoxes (retrieval). It supports the
OWL-API, the lisp-API and the DIG interface.
44
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (3)
• fuzzyDL
– is a free Java/C++ based reasoner for fuzzy SHIF with concrete
fuzzy concepts (explicit definition of fuzzy sets + modifiers). It
implements a tableau + Mixed Integer Linear Programming
optimization decision procedure to compute the maximal degree
of subsumption and instance checking w.r.t. a general TBox and
Abox. It supports Zadeh semantics, Lukasiewicz semantics and is
backward compatible with classical description logic reasoning.
• HermiT
– is a free (under LGPL license) Java reasoner for SHIQ with
description graphs. It implements a hypertableau-based decision
procedure for general TBoxes and description graphs. It uses the
KAON2 API.
45
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (4)
• Hoolet
– reasons over OWL-DL ontologies by translating them to full firstorder logic and then applying a first-order theorem prover.
• KAON2
– is a free (free for non-commercial usage) Java reasoner for SHIQ
extended with the DL-safe fragment of SWRL. It implements a
resolution-based decision procedure for general TBoxes
(subsumption, satisfiability, classification) and ABoxes (retrieval,
conjunctive query answering). It comes with its own, Java-based
interface, and supports the DIG interface.
46
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (5)
• MSPASS
– is a free open-source C reasoner for numerous description logics.
It implements a resolution-based decision procedure for
extensions of ALB (which is ALC with inverse and Boolean
operators on roles) with general TBoxes (satisfiability,
subsumption) and ABoxes (instance checking, retrieval). It is an
extension of the theorem prover SPASS, and can thus also be used
to reason about arbitrary first-order statements.
• AllegroGraph
– is a disk-based RDF Database, that aims at providing a solid
storage layer for powerful geotemporal reasoning, social network
analytics and ontology modeling capabilities for today's Semantic
Technology applications.
47
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (6)
• Jena
– an open source semantic web framework for Java which includes
a number of different semantic reasoning modules.
• SweetRules
– an integrated set of tools for Semantic web rules and ontologies.
48
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (7)
• OWLIM
– a high-performance semantic repository developed in Java and
available in two versions: free SwiftOWLIM and commercial
BigOWLIM. Supports a subset of OWL-Lite semantics, which can
be configured through rule-set definition and selection.
• Pellet
– is a free open-source Java-based reasoner for SROIQ with simple
datatypes (i.e., for OWL 1.1). It implements a tableau-based
decision procedure for general TBoxes (subsumption, satisfiability,
classification) and ABoxes (retrieval, conjunctive query
answering). It supports the OWL-API, the DIG interface, and the
Jena interface and comes with numerous other features.
49
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (8)
• Owlgres
– is a reasoner for the DL Lite sub-language of OWL 2. It is based on
the PostgreSQL relational DBMS. Besides the open source license
AGPL, Owlgres can also be obtained via a commercial licensing
model.
• QuOnto
– is a free (for non-commercial use) Java-based reasoner for DL-lite
with GCIs. It implements a query rewriting algorithm for both
consistency checking and query answering for unions of
conjunctive queries over DL-Lite knowledge bases, whose ABox is
managed through relational database technology. It comes with
its own Java-based interface.
50
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (9)
• RacerPro
– is a commercial (free trials and research licenses are available)
lisp-based reasoner for SHIQ with simple datatypes (i.e., for OWLDL with qualified number restrictions, but without nominals). It
implements a tableau-based decision procedure for general
TBoxes (subsumption, satisfiability, classification) and ABoxes
(retrieval, nRQL query answering). It supports the OWL-API and
the DIG interface and comes with numerous other features.
• SHER
– is a commercial (free for academic use) Java-based reasoner for
SHIN. It is based on Pellet and uses database technology to reason
about SHIN TBoxes and ABoxes (retrieval, conjunctive query
answering).
51
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (10)
• SoftFacts
– is a free Java-based reasoner for fuzzy DLR-lite. It implements a
query rewriting approach to answer conjunctive queries over a
DLR-lite TBox, where the data is stored in a database (MySQL,
Postgres and RankSQL). It also supports top-k retrieval (find top-k
scored tuples satisfying a query).
• KAONP2P
– is a semantics-based P2P system - based on the KAON2 ontology
management system. KAONp2p provides distributed reasoning
capabilities for the expressive web ontology language OWL, along
with a peer selection process to identify relevant knowledge
sources in the peer network.
52
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (11)
• SimDL
– is an open Java-based similarity reasoner for various description
logics (from the ALC family (up to ALCHQ)). The reasoner can be
used via DIG or a Protégé plug-in called SimCat. SIM-DL also
supports classical subsumption reasoning and satisfiability
checking.
• DLog
– Resolution based Description Logic ABox reasoner that translates
to Prolog.
53
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (12)
• MARVIN
– Is a parallel and distributed platform for processing large amounts
of RDF data, on a network of loosely coupled peers. Marvin is
based on the approach of divide-conquer-swap.
54
Ontology Reasoning - Majid Sazvar - 2010
Overview of DL Reasoners (13)
• DL reasoners which are no longer actively supported:
– BACK, CLASSIC, CICLOP, CRACK, DLP, FaCT, FLEX, HAM-ALC, K-REP, KRIS,
LOOM, SAT, YAK, Instance Store, … .
55
Ontology Reasoning - Majid Sazvar - 2010
Most scalable engines
•
•
•
•
•
Oracle
OWLIM
MARVIN
SHER
AllegroGraph
56
Current Researches
Ontology Reasoning - Majid Sazvar - 2010
Current Researches
• Extending Description Logics
– Complex roles
– Future OWL extensions (e.g., with “rules”)
• Integrating with other logics/systems
• Alternative reasoning techniques
– Automata based algorithms
– Translation into datalog
– Graph based algorithms (for sub ALC languages)
58
Ontology Reasoning - Majid Sazvar - 2010
Current Researches (2)
• Improving Scalability
– Very large ontologies
– Very large numbers of individuals
• Other reasoning tasks (non-standard inferences)
– Matching, explanation, querying, …
• Implementation of tools and Infrastructure
– More expressive languages (such as SHOIN)
– New algorithmic techniques
– Tools to support for large scale ontological engineering
• Editing, visualisation, etc.
59
?