Transcript Powerpoint

The Model Evolution Calculus and an
Application to Ontological Reasoning
Peter Baumgartner
Max-Planck-Institute for Informatics
Saarbrücken,Germany
Joint work with Cesare Tinelli, U Iowa
Background – Instance Based Methods
• Model Evolution is related to Instance Based Methods
– Ordered Semantic Hyper Linking [Plaisted et al]
– Primal Partial Instantiation [Hooker et al]
– Disconnection Method [Billon], DCTP [Letz&Stenz]
– Inst-Gen [Ganzinger&Korovin]
– First-Order DPLL [B.]
• Principle: Reduce proof search in first-order (clausal) logic to
propositional logic in an „intelligent“ way
• Different to Resolution, Model Elimination,…
(Pro‘s and Con‘s)
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
2
Background - DPLL
• The best modern SAT solvers (satz, MiniSat, zChaff, Berkmin,…) are
based on the Davis-Putnam-Logemann-Loveland procedure
[DPLL 1960-1963]
• Can DPLL be lifted to the first-order level?
Can we combine
– successful SAT techniques
(unit propagation, backjumping, learning,…)
– successful first-order techniques?
(unification, subsumption, ...)?
• Model Evolution (ME) and its predecessor First-Order DPLL do so
• ME different to Resolution, Tableaux and Model Elimination
but related to "Instance Based Methods"
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
3
DPLL procedure
Input: Propositional clause set
Output: Model or „unsatisfiable”
Algorithm components:
- Propositional semantic tree
enumerates interpretations
- Simplification
- Split
- Backtracking
Lifting to first-order logic?
A
B
C
: A
: B
: C
?
f A, Bg j= : A _ : B _ C _ D, : : :
No, split on C:
f A, B, Cg j= : A _ : B _ C _ D, : : :
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
4
Model Evolution as First-Order DPLL
Lifing of semantic tree data structure and derivation rules to first-order
Input: First-order clause set
Output: Model or „unsatisfiable”
if termination
Algorithm components:
- First-order semantic tree
enumerates interpretations
- Simplification
- Split
- Backtracking
v is a "parameter"
P(a, v)
: P(a, b)
: P(a, v)
P(a, b)
?
f P(a, v), : P(a, b)g j= Q(x, y) _ P(x, y)
Interpretation induced by a branch?
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
5
Interpretation Induced by a Branch
A branch literal specifies the truth value of its ground instances unless
there is a more specific branch literal with opposite sign
: v
Branch:
f : v, P(a, z), : P(a, b)g
P(a, v)
Induced Interpretation
true: P(a, a)
false: P(a, b), Q(a, b)
: P(a, b)
How to determine Split literal?
Calculus?
Q(a, b)
: P(a, v)
P(a, b)
: Q(a, b)
?
f : v, P(a, v), : P(a, b)g j= Q(x, y) _ P(x, y)
No, because
)
f : v, P(a, v), : P(a, b)g 6
j= Q(a, b) _ P(a, b)
Split with Q(a, b) to satisfy P(a, b) _ Q(a, b)
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
6
Model Evolution Calculus
• Branches and clause sets may shrink as the derivation proceeds
• Such dynamics is best modeled with a sequent style calculus:
¤ ` ©
Current Clause Set
Context: A set of literals
(the „current branch“)
• Derivation Rules
– To simplify the clause set , to simplify the context 
– Splitting
– Close
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
7
Derivation Rules – Simplified (1)
Split
¤ ` ©, C _ L
¤, L¾ ` ©, C _ L
¤, L¾ ` ©, C _ L
if
1. ¾ is a simultaneous mgu of C _ L against ¤,
2. neither L¾ nor L¾ is contained in ¤, and
3. L¾ contains no variables (parameters OK)
¤: P(u, u)
Q(v, b)
C _ L : : P(x, y) _ : Q(a, z)
¾ = f x !7 u, y 7
! u,
v7
! a, z !7 b g
(C _ L)¾ : : P(x, x) _ : Q(a, b)
2. violated
2. satisfied
L¾ = : Q(a, b) is admissible for Split
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
8
Derivation Rules – Simplified (2)
Close
¤
¤
`
`
©, C
?
if
1. © 6
= ; or C 6
= ?
2. there is a simultaneous mgu ¾ of C against ¤ such that
¤ contains the complement of each literal of C¾
¤: P(u, u)
Q(a, b)
C : : P(x, y) _ : Q(a, z)
¾= f x 7
! u, y 7
! u, z 7
! bg
C¾ : : P(x, x) _ : Q(a, b)
2. satisfied
2. satisfied
Close is applicable
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
9
Derivation Rules – Simplification Rules (1)
Propositional level:
Subsume
¤, L `
¤, L `
©, L _ C
©
First-order level ¼ unit subsumption:
- All variables in context literal L must be universally quantified
- Replace equality by matching
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
10
Derivation Rules – Simplification Rules (2)
Propositional level:
Resolve
¤, L `
¤, L `
©, L _ C
©, C
First-order level ¼ restricted unit resolution
- All variables in context literal L must be universally quantified
- Replace equality by unification
- The unifier must not modify C
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
11
Derivation Rules – Simplification Rules (3)
Compact
¤, K, L `
¤, K
`
©
©
if
1. all variables in K are universally quantified
2. K¾ = L, for some substitution ¾
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
12
Derivations and Completeness
: v ` Input clause set
Fairness
Closed tree or open limit tree,
with some branch satisfying:
¤ 1 ` ©1
¤ 2 ` ©2
closed
¤ n ` ©n
¤ 1 :=
©1 :=
S
S
T
i¸ 0
i¸ 0
T
j¸ i
¤j
j¸ i
©j
1. Close not applicable to any ¤ i
2. For all C 2 ©1 and subst. ° ,
``if for some i, ¤ i 6
j= C°
then there is j ¸ i
such that ¤ j j= C°
(Use Split to achieve this)
Complet eness
Suppose a fair derivation
that is not a closed tree
Show that ¤ 1 j= ©1
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
13
Implementation: Darwin
• „Serious“ Implementation
Part of Master Thesis, will be continued in Ph.D. project
• (Intended) Applications
• detecting dependent variables in CSP problems
• strong equivalence of logic programs
• Bernays-Schoenfinkel fragment of autoepistemic logic
• Currently extended:
• Lemma learning
• Equality inference rules
• Written in OCaml, 14K LOC
• User manual, proof tree output (GraphViz)
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
14
Darwin Performance
Results of ATP system competition at IJCAR 2004
MIX: Clause logic with Equality
EPR: function free clause logic (without Equality)
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
15
Application: Ontological Reasoning
• Automated reasoning on formal ontologies is of growing interest
• Description logics are a widely used logical formalism, e.g. OWL
9 partOf
AuthoredChapter
9 hasPart
AuthoredChapter v
CollectionBook v
CollectionBook
9 partOf : CollectionBook
9 hasPart : AuthoredChapter
• Highly optimized reasoners for decidable DLs can cope with
realistically sized ontologies (FaCT, Racer)
• Can one also use Darwin/off-the-shelf provers?
• And why?
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
16
Why? Going Beyond Description Logics
DL + Rules:
9 partOf
AuthoredChapter
9 hasPart
AuthoredChapter
CollectionBook
v
v
:::
EditorIsAuthor(x) Ã
CollectionBook
9 partOf : CollectionBook
9 hasPart : AuthoredChapter
CollectionBook(x) ^ hasPart(x, y) ^
hasAuthor(y, z) ^ hasEditor(x, z)
• Rules cause undecidability
• Cannot use DL reasoner
• Translate to first-order logic and use theorem prover
• How? (Naive approach fails)
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
17
How? Our Approach
DL
First-Order Logic
Facts
Rules
Query
Clause Normalform
Equality
Needed for efficiency / termination
Blocking
Clause Logic
Darwin
Model Evolution
8 (L1 _ ¢¢¢_ Ln ), where Li (negated) atom
Result
- "Unsatisfiable"
- "Model"
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
KRHyper
Tableaux
18
Equality
Work in collaboration with Master's student
Equality comes in, e.g., in the translation of
– nominals ("oneOf")
WhiteLoire v 8 madeFromGrape : Sauvignon t Chenin t Pinot
WhiteLoire(x) ^ madeFromGrape(x, y) )
y = Sauvignon _ y = Chenin _ y = Pinot
– cardinality restrictions
Cation v
· 4 hasCharge
Cation(x) ^ hasCharge(x, x1) ^ ¢¢¢^ hasCharge(x, x5) )
x1 = x2 _ x1 = x3 _ ¢¢¢_ x4 = x5
-> Need an (efficient) way to treat equality
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
19
Equality
• Options: equality axioms - builtin in prover - by transformation
• Our transformation:
Given clause:
c= d
Ã
Our trafo:
c= d Ã
f(x) = b ^ x = a
+ ref, sym, trans
[Brand 1975]:
c= d
d= c
+ ref
Ã
Ã
f(a) = b
f(x) = y ^ x = a ^ y = b
f(x) = y ^ x = a ^ y = b
- Brand's transformation is theoretically more attractive
- But advantages do not apply for "typical" ontologies
- In practice, our transformation works much better
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
20
Blocking
• Problem: Termination in case of satisfiable input.
Caused by certain DL language constructs and cyclic definitions:
9 hasAuthor
AuthoredChapter
9 hasPart
CollectionBook
• Solution: Idea: Re-use old individual to satisfy  -quantifier.
Technical: encode search for finite domain model in clause set:
aC(hP(hA(a))) ^ hP(hA(a)) = a
aC(a) ^ dom(a)
Try this first
aC(hP(hA(a))) ^ dom(hP(hA(a)))
• Issue: Search space reduction: don't speculate all possible equalities
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
21
o
Experimental Evaluation – OWL Test Cases from W3C
Consist ent
56 problems
Inconsist ent
72 problems
Ent ailment
57 problems
Darwin +blocking
Darwin - blocking
KRHyper +blocking
KRHyper - blocking
89%
7%
86%
75%
92%
94%
89%
94%
89%
93%
93%
93%
Darwin [ KRHyper
Hoolet (Vampire)
Surnia (Otter)
Euler ("Prover")
Fact (DL)
Pellet (DL)
OWLP (DL)
Cerebra (DL)
FOWL (OWL)
ConsVISor (OWL-full)
93%
78%
0%
42%
96%
50%
90%
53%
77%
94%
94%
0%
98%
85%
98%
26%
59%
4%
65%
93%
72%
13%
100%
7%
86%
53%
61%
32%
-
Syst em
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
22
Conclusions
• Objective: "robust" reasoning support beyond description logics:
– Equality treatment
– Blocking (decides standard services for cyclic ALC TBoxes)
– It's not only "strategy hacking" – need theoretical results
– Competitive with DL systems on common domain
• "Rules" not benchmarked (no benchmarks available),
but they turned out to be very useful in own application projects:
– Reputational risk management
– Document management (E-Learning)
– Upper ontology for computational linguistic application
• Nonmonotonic negation of KRHyper very useful
How to integrate it in Model Evolution?
A First-Order Davis-Putnam Procedure and its Application to Ontological Reasoning
23