Transcript CSE 291

Department of Computer Science & Engineering
University of California, San Diego
CSE-291: Ontologies in Data Integration
Spring 2003
Bertram Ludäscher
[email protected]
• Tableaux calculus II, introduction to the LeanTAP prover
• Example: Reasoning about concepts with LeanTAP
• Definitorial terminologies, terminological cycles
•BREAK
• Q&A to Assignments
CSE-291: Ontologies in Data Integration
(Semantic) Tableaux Rules
• () rule for F = A  B
• () rule for F = A  B
• () rule for F = x: A(X,...)
– substitute a -variable X with an
arbitrary term t
t arbitrary
c new
• () rules for F = x: A(X,...)
– substitute a -variable X with a new
constant c
• A branch is closed if it contains complementary formulas
• A tableaux is closed if every branch is closed
CSE-291: Ontologies in Data Integration
FO Tableaux Calculus
Theorem (Soundness, Completeness of Tableaux
calculus):
Let A1,..., Ak and F be first-order logic sentences.
(Recall: a sentence is a closed formula, i.e., has no free variables)
Then the following are equivalent:
1. A1, ..., Ak |= F
2. A1  ...  Ak  F is unsatisfiable (inconsistent)
3. There is a closed tableaux for {A1, ..., Ak ,  F}
CSE-291: Ontologies in Data Integration
Example Revisited
(Assumption)
• Initial Example in FO logic
• How can we prove it in the Tableaux Calculus?
CSE-291: Ontologies in Data Integration
Partially closed
tableaux
[Becker&Haehnle, Automatisches Beweisen, 2001]
CSE-291: Ontologies in Data Integration
Description Logic Revisited
Basic description logic
Source: [F. Baader, W. Nutt. Basic Description Logics. Description
Logic Handbook, Cambridge University Press, 2002].
• a whole family of DLs is obtained by adding
– full existential quantification R.C
– union
– ...
CSE-291: Ontologies in Data Integration
... Reasoning with the Family ...
• concept definition: MyConcept  DL-formula
• concept inclusion: MyConcept  DL-formula
• finite set of definitions is a terminology or TBox if for every
atomic concept A there is at most one axiom whose lhs is A
CSE-291: Ontologies in Data Integration
Definitorial Terminologies
• In a Tbox T we distinguish: primitive concepts (occurring only on
rhs) and defined concepts (occurring on lhs)
• T is definitorial if every interpretation of primitive concepts yields
exactly one model of T (and thus for the defined concepts)
 meaning of defined concepts is fixed once the primitive concepts are
interpreted !
• A directly uses B in T if B appears in the rhs of the definition of A
• A uses B is the transitive closure of ‘directly uses’
• T is cyclic if A uses A for some A; else acyclic
One can show:
If T is acyclic then T is definitorial
What about this one?
CSE-291: Ontologies in Data Integration
Expansion of Terminologies
• For acyclic T we can “unfold” concept definitions until
every defined concepts is specified in terms of
primitive concepts only
 the expansion of a Tbox T
• Example:
CSE-291: Ontologies in Data Integration
Reasoning in the Tableaux calculus
From this
Tbox
We want to show this
Expansion
In First-order (LeanTap) syntax
CSE-291: Ontologies in Data Integration
LeanTap Demo
CSE-291: Ontologies in Data Integration
Computing the Negation Normal Form
• LeanTap Tableaux Prover:
–
–
–
–
CSE-291: Ontologies in Data Integration
{Axioms} & –( Theorem )
 FO formula
 formula in NNF
 attempt to close tableaux
The Sound and
Complete LeanTap
Tableaux Prover
CSE-291: Ontologies in Data Integration
How LeanTAP works
• (1) select A; put B in
unexpanded list
• (3) split branch;
creates two new goals
• (6) create new
instance (X1) from
(X) formula, add X1
to free vars; or
backtrack if varlimit
is reached
• (11) close branch for
literals; recurse
CSE-291: Ontologies in Data Integration
The Sound and
Complete LeanTap
Tableaux Prover
CSE-291: Ontologies in Data Integration
Reasoning in Database Mediation
• View expansion in Global-as-View mediation is similar to this
concept expansion
– uncle(X, Y) :- parent(X, Z), brother(Z, Y)
; parent(X, Z), brother_in_law(Z, Y).
– aunt(X, Y) :- parent(X, Z), sister(Z, Y)
; parent(X, Z), sister_in_law(Z, Y).
– parent(X, Y) :- father(X, Y)
; mother(X, Y).
– brother_in_law(X, Y) :- sister(X, Z), spouse(Z, Y)
; spouse(X, Z), brother(Z, Y).
...
• Goal: find a “query plan” that expresses the derived relation
uncle/2 in terms of only base relations (father/2, mother/2, ..)
CSE-291: Ontologies in Data Integration
Querying vs. Reasoning
• Querying:
– given a DB instance I (= logic interpretation), evaluate a query
expression (e.g. SQL, FO formula, Prolog program, ...)
– boolean query: check if I |= 
(i.e., if I is a model of )
– (ternary) query: { (X, Y, Z) | I |=  (X,Y,Z) }
=> check happyFathers in a given database
• Reasoning:
– check if I |=  implies I |=  for all databases I,
– i.e., if  => 
– undecidable for FO, F-logic, etc.
– Descriptions Logics are decidable fragments
 concept subsumption, concept hierarchy, classification
 semantic tableaux, resolution, specialized algorithms
CSE-291: Ontologies in Data Integration
Mediator Demo: query/view rewriting
(aka planning) is reasoning!
CSE-291: Ontologies in Data Integration
Querying (a database) is formula evaluation
(aka running the query)
CSE-291: Ontologies in Data Integration