Fitting Horn DL Ontologies to ABox and Query Examples: A Tale of Simulation Quantifiers and Finite Models

Proof.‘1 ⇒ 2’

there exists a completionCofA − such that (a)Q(a)̸∈ Cfor each(A, Q(a))∈E −; (b) if (A, Q(a))∈E + and (A, a)⪯ L (C, b), then Q(b)∈ C. Proof.‘1 ⇒ 2’. Suppose that E admits a fitting L- ontology O. Then for every e= (A, Q(a))∈E − there is a model Ie of A and O with Ie ̸|=Q(a) . Since L- ontologies are invariant under disjoint union, the interpre- tation I= U...

This is only possible if L ∈ {EL ⊥,ELI ⊥} because then simulations are required to be total

There is noL-simulation fromAtoC. This is only possible if L ∈ {EL ⊥,ELI ⊥} because then simulations are required to be total. As in the ‘(ii)⇒(i)’ direction of the proof of Theorem 1, we find an aA ∈ ind(A)such that for allb∈ind(C), (A, aA)̸⪯ ℓ L (A+, b) whereℓ=|C| · |A|. We then set Oe :={C ℓ,L A,aA ⊑ ⊥}

We set Oe :={C ℓ,L A,a ⊑Q}, whereℓ=|C| · |A|

There is anL-simulation fromAtoC. We set Oe :={C ℓ,L A,a ⊑Q}, whereℓ=|C| · |A|. We show that O:= S e∈E+ Oe fits E. For each e= (A, Q(a))∈E +, we have A ∪ Oe |=Q(a) , thus A ∪ O |= Q(a) as required. In both cases this is due to b∈(C ℓ,L A,b)J for all modelsJofAand individualsb∈ind(A). Next consider a negative example e= (A, Q(a))∈E −. Let IC be C viewed as...

If I is an L-forest model of A, then I |=p if and only if there exists an L-forest A-variation p′ of p such that I |=p ′

Proof.We start with Point 1

for every L-forest A-variation p′ of p: I |=p ′ if and only ifI |=bp♯ for allbp♯ ∈red(p ′). Proof.We start with Point 1. ‘only if’. Let I be an L- forest model of A and suppose that I |=p , witnessed by a homomorphism g from p to I. Using g, we construct an L- forest A-variation p′ of p as follows. First, for every variable x with g(x) =a∈ind(A) , replace...

there is anL-ontology that fitsE

there exists a finite interpretationIsuch that (a)I= U e∈E− Ie where, for each e= (A, q)∈E −, Ie is a model ofAwithI e ̸|=q; (b) for all (A, q)∈E +: if S is an L-simulation from A to I, thenI A,S,L |=q. To prove the theorem, we need a way to handle the non- rooted parts of the queries in Condition (b) uniformly when constructing a fitting ontology from a ...

2018

Observe that then L=L ′ ⊥ ∈ {EL ⊥,ELI ⊥} and there exists an indi- vidual a∈ind(A) such that (A, a)̸⪯ L′ (I, d), for all d∈∆ I

There exists no L-simulation from A to I. Observe that then L=L ′ ⊥ ∈ {EL ⊥,ELI ⊥} and there exists an indi- vidual a∈ind(A) such that (A, a)̸⪯ L′ (I, d), for all d∈∆ I. To guarantee that the constructed ontology fits such an example, we must ensure that A is inconsistent withO. Hence, we set ens(e) :={⊥(a)}

By assumption and Lemma 10, there exists some rooted CQ p in q and an L-forest A-variation p′ of p such that IA,S,L |=p ′

Otherwise, let S be the maximal L-simulation from A to I. By assumption and Lemma 10, there exists some rooted CQ p in q and an L-forest A-variation p′ of p such that IA,S,L |=p ′. Since S is chosen to be maxi- mal, it suffices to ensure that A ∪ O entails the reduc- tion queries of p′. For each existential reduction query bp♯ =∃x C(x)∈red(p ′), let abp♯ ...

there exists a finite interpretation I that satisfies Condi- tions (a′) and (b′) of Lemma 7

memorized

for every e∈E + there exists an Oe ∈Γ e such that A ∪S e∈E− Oe ̸|=fin p′ for every (A, q)∈E − and L- forestA-variationp ′ of a CQ inq. ‘1⇒ 2’ Assume there exists finite modelI that satisfies Conditions (a′) and (b′) of Lemma 7. Since I satisfies Con- dition (b′), for every e∈E + there exists an Oe ∈Γ e such that I |=S e∈E+ Oe. Let e= (A, q)∈E −, and Ie be...

2004