$$%% examples \newcommand{\exGraph}{\graph_{\mathrm{ex}}} \newcommand{\exOnto}{\onto_{\mathrm{ex}}} \newcommand{\exMappings}{\mappings_{\mathrm{ex}}} \newcommand{\exExtensions}{\extensions_{\mathrm{ex}}} \newcommand{\exRule}{r_{\mathrm{ex}}} \newcommand{\RDFSrules}{\rules_{\mathrm{RDFS}}} %% RDF \newcommand{\triple}[3]{(#1, #2, #3)} \newcommand{\tuple}[1]{\langle #1 \rangle} \newcommand{\subject}{\mathtt{s}} \newcommand{\prop}{\mathtt{p}} \newcommand{\object}{\mathtt{o}} \newcommand{\blank}{\_{:}b} \newcommand{\blankn}[1]{\_{:}#1} \newcommand{\irin}[1]{{:}\mathrm{#1}} \newcommand{\class}{\mathtt{c}} \newcommand{\nsrdf}{\mathrm{rdf{:}}} \newcommand{\nsrdfs}{\mathrm{rdfs{:}}} \newcommand{\rdftype}{\mathrm{rdf{:}type}} \newcommand{\rdfLiteral}{\mathrm{rdf{:}Literal}} \newcommand{\rdfssubClassOf}{\mathrm{rdfs{:}subClassOf}} \newcommand{\rdfssubPropertyOf}{\mathrm{rdfs{:}subPropertyOf}} \newcommand{\rdfsdomain}{\mathrm{rdfs{:}domain}} \newcommand{\rdfsrange}{\mathrm{rdfs{:}range}} \newcommand{\rdfsClass}{\mathrm{rdfs{:}Class}} \newcommand{\rdfProperty}{\mathrm{rdf{:}Property}} \newcommand{\xsdint}{\mathrm{xsd{:}int}} %% \newcommand{\type}{\tau} \newcommand{\subclass}{\prec_{sc}} \newcommand{\subproperty}{\prec_{sp}} \newcommand{\domain}{\hookleftarrow_{d}} \newcommand{\range}{\hookrightarrow_{r}} \newcommand{\rdfentailment}{\vdash_{^\mathrm{RDF}}} \newcommand{\RDFS}[1]{\mathrm{RDFS}(#1)} \newcommand{\aka}{a.k.a.~} \newcommand{\etc}{etc} \newcommand{\wrt}{w.r.t.~} \newcommand{\st}{s.t.~} \newcommand{\ie}{i.e.,~} \newcommand{\eg}{e.g.,~} \newcommand{\graph}{G} \newcommand{\rules}{\mathcal{R}} \newcommand{\sources}{\mathcal{S}} \newcommand{\views}{\mathcal{V}} \newcommand{\extensions}{\mathcal{E}} \newcommand{\onto}{\mathcal{O}} \newcommand{\mappings}{\mathcal{M}} \newcommand{\modelsrdf}{\models_\rules} \newcommand{\bgp}{P} \newcommand{\Bl}[1]{\mathrm{Bl}(#1)} \newcommand{\Val}[1]{\mathrm{Val}(#1)} \newcommand{\Var}[1]{\mathrm{Var(#1)}} \newcommand{\ext}[1]{\mathrm{ext}(#1)} \newcommand{\cert}{\mathrm{cert}} \newcommand{\ans}{\mathrm{ans}} \newcommand{\query}{\leftarrow} \newcommand{\body}[1]{\textrm{body}(#1)} \newcommand{\head}[1]{\textrm{head}(#1)} \newcommand{\cs}{\mathrm{cs}} \newcommand{\lcs}{\mathrm{lcs}} \newcommand{\cl}{\mathrm{cl}} \newcommand{\lua}{\mathrm{lua}} \newcommand{\lur}{\mathrm{lur}} \newtheorem{lemma}{Lemma} \newtheorem{definition}{Definition} \newtheorem{problem}{Problem} \newtheorem{property}{Property} \newtheorem{corollary}{Corollary} \newtheorem{example}{Example} \newtheorem{theorem}{Theorem} \newcommand{\URIs}{\mathscr U} \newcommand{\IRIs}{\mathscr I} \newcommand{\BNodes}{\mathscr B} \newcommand{\Literals}{\mathscr L} \newcommand{\Variables}{\mathscr V} % DB \newcommand{\CQ}{\ensuremath{\mathtt{CQ}}\xspace} \newcommand{\UCQ}{\ensuremath{\mathtt{UCQ}}\xspace} \newcommand{\SQL}{\ensuremath{\mathtt{SQL}}\xspace} \newcommand{\rel}[1]{\mathsf{#1}} % Cost model \newcommand{\cans}[1]{|#1|_t} \newcommand{\cref}[1]{|#1|_r} \newcommand{\db}{\mathtt{db}} % DL \newcommand{\cn}{\ensuremath{N_{C}}\xspace} \newcommand{\rn}{\ensuremath{N_{R}}\xspace} \newcommand{\inds}{\ensuremath{N_{I}}\xspace} \newcommand{\ainds}{\ensuremath{\mathrm{Ind}}\xspace} \newcommand{\funct}{\mathit{funct} \ } \newcommand{\KB}{\mathcal{K}\xspace} \newcommand{\dlr}{DL-Lite$_{\mathcal{R}}$\xspace} % Logics \newcommand{\FOL}{\ensuremath{\mathtt{FOL}}\xspace} \newcommand{\datalog}{\ensuremath{\mathtt{Datalog}}\xspace} \newcommand{\dllite}{DL-Lite\xspace} \newcommand{\true}{\mathrm{true}} \newcommand{\false}{\mathrm{false}} \newcommand{\dis}{\mathtt{dis}} \newcommand{\vars}[1]{\ensuremath{\mathrm{vars}(#1)}} %\newcommand{\terms}[1]{\ensuremath{\mathrm{terms}(#1)}} %math \renewcommand{\phi}{\varphi} \newcommand\eqdef{\stackrel{\mathclap{\normalfont\mbox{def}}}{=}} \newcommand\restr[2]{#1_{|#2}} \newcommand{\ontoBody}[1]{\mathrm{body}_\onto(#1)} %proof of the rewriting theorem \newcommand{\rdfGraph}{\graph^{\mappings}_{\extensions}} \newcommand\systemGraph{\graph^{\mappings \cup \mappings^{\text{STD}}_\onto}_{\extensions \cup \extensions_\onto}} \newcommand\viewsGraph{\graph^{\mappings^{\rules,\onto} \cup \mappings^{\text{STD}}_\onto}_{\extensions \cup \extensions_\onto}} \newcommand{\standMappings}{\mappings^{\text{STD}}_\onto} \newcommand{\reminder}[1]{[\vadjust{\vbox to0pt{\vss\hbox to0pt{\hss{\Large $\Longrightarrow$}}}}{{\textsf{\small #1}}}]} %\newcommand{\FG}[1]{\textcolor{blue}{\reminder{FG:~#1}}} \newcommand{\extVersion}{false} \newcommand{\printIfExtVersion}[2] { \ifthenelse{\equal{\extVersion}{true}}{#1}{} \ifthenelse{\equal{\extVersion}{false}}{#2}{} } \newcommand{\bda}{\true} \newcommand{\ifBDA}[2]% {% \ifthenelse{\equal{\bda}{true}}{#1}{}% \ifthenelse{\equal{\bda}{false}}{#2}{}% } %%% Local Variables: %%% TeX-master: "paper" %%% End: $$

Extended Reasoning Rules Support in GLAV Integration

The aim of this paper is to extend the reasoning capability in GLAV Integration in the following general context where:

We want to find some minimal restrictions on \(\rules\), such that we can find \(\mappings^{\rules}\) an equivalent set of GLAV mappings on source schema \(S\) and on global schema \(G\) i.e. for each \(I\) instance of \(S\), \(U\) is an instance of \(G\) such that \(I, \mappings, \rules \models U\) if and only if \(I, \mappings^{\rules} \models U\).

Examples

A series of examples to show how we can go further than mappings head saturation.

Examples of Extensions

Saturation on Several Mappings

\[\mappings = \{ V_{1}(x) \leadsto A(x), V_{2}(x) \leadsto B(x) \}\]

\[\rules = \{ A(x) \wedge B(x) \rightarrow C(x) \}\]

Here, we need to use two mappings at the same time to fully reason with \(r\). In order to handle it, we can define \(\mappings^{\rules}\) as the set of GLAV mappings containing mappings of \(\mappings\) and the following mapping:

\[V_{1}(x) \wedge V_{2}(x) \leadsto C(x)\]

Mismatch with Constant in Rule

\[\mappings = \{m: V(x,y) \leadsto T(x,y) \}\]

\[\rules = \{ r: T(x, C_{1}) \rightarrow T(x, C_{2}) \}\]

We can not apply \(r\) on the head of \(m\) in a saturation of conjunctive query on context like in cite:HassadLearningCommonalitiesSPARQL2017. To solve this issue, we should handle the case, where \(y\) is \(m\) is equals to \(C_{1}\). We can do it by defining a new mappings:

\[m^{r}: V(x, C_{1}) \leadsto T(x, C_{2})\]

and by defining \(\mappings^{\rules}\) as \(\{m, m^{r}\}\).

This situation doesn't appear in cite:BuronRewritingBasedQueryAnswering2018a, because mapping heads and rules are build such that variables and constant are in the same position in triple.

Examples of Limits

Rule for Transitivity

\[\mappings = \{ m: V(x,y) \leadsto C(x,y) \}\]

\[\rules = \{ r: C(x, y) \wedge C(y, z) \rightarrow C(x, z) \}\]

In this case, we can wrap two mappings \(m\) with rule \(r\) given the following mapping:

\[m': V(x,y) \wedge V(y,z) \leadsto C(x,z)\]

Then, we can continue to wrap this mapping and \(m\) with \(r\) etc.

Simple RDFS Entailment Rule

\[\mappings = \{m_{t}: V_{t}(x,y) \leadsto T(x,y), m_{c}: V_{c}(x,y) \leadsto C(y_{1}, y_{2}) \}\]

\[\rules = \{ r: T(x, y_{1}) \wedge C(y_{1}, y_{2}) \rightarrow T(x, y_{2}) \}\]

We can view above definitions as an RDFS integration system, where \(m_{t}\) (resp. \(m_{c}\)) populates the global schema with triples form \(\triple{x}{\type}{y}\) (resp. \(\triple{y_{1}}{\subclass}{y_{2}}\)). And the rule \(r\) can be viewed as \(\triple{x}{\type}{y_{1}} \wedge \triple{y_{1}}{\subclass}{y_{2}} \rightarrow \triple{x}{\type}{y_{2}}\).

Wrapping together \(m_{t}\) and \(m_{c}\) using \(r\) will produce the following mapping:

\[V_{t}(x,y_{1}) \wedge V_{c}(y_{1}, y_{2}) \leadsto T(x,y_{2})\]

We can wrap this mappings with \(m_{c}\) using \(r\), by continuing we will produce mappings of the form:

\[V_{t}(x,y_{1}) \wedge V_{c}(y_{1}, y_{2}) \dots \wedge V_{c}(y_{n-1}, y_{n}) \leadsto T(x, y_{n})\]

This case doesn't appear in the setting of cite:BuronRewritingBasedQueryAnswering2018a, because we demand that mapping heads contain IRIs in class position.

Definitions

We now want to formalize the definition of wrapping a mapping set with a rule. As defined in cite:MugnierIntroductionOntologyBasedQuery2014a, we will use the definition piece unifier of a query with a rule. We will use this definition to find piece unifier of rule body in \(\rules\) with mapping from \(\mappings\) (considering as existential rules). We can illustrate \(u\) a piece unifier of the body of the rule \(B(\bar v_{1}, \bar v_{2}) \rightarrow H(\bar v_{2}, \bar v_{3})\) with the head of mapping \(q_{1}(\bar x) \leadsto q_{2}(\bar x)\) by:

\[q_{1}(\bar x) \leadsto q_{2}(\bar x) \stackrel{u}{\leftrightarrow} B(\bar v_{1}, \bar v_{2}) \rightarrow H(\bar v_{2}, \bar v_{3})\] such that \(u(q_{2}(\bar x)) \subseteq u(B(\bar v_{1}, \bar v_{2}))\).

Given one rule \(r\in \rules\) and mappings \(m_{1}, m_{2}, \dots, m_{n}\) such that:

  1. there exists for \(1 \leq i \leq n, u_{i}\) a piece unifier of the head of \(r\) with \(m_{i}\).
  2. piece unifiers \(u_{1}, u_{2}, \dots u_{n}\) are compatible and \(\{u_{1}(\head{m_{1}}), \dots, u_{n}(\head{m_{n}})\}\) forms a partition of \(u_{1}(u_{2}( \dots u_{n}(\body{r}))\dots)\)

The mapping resulting of wrapping mappings \(m_{1}, \dots, m_{n}\) together with the rule \(r\) is defined by:

\[\bigwedge_{1 \leq i \leq n} u_{i}(\body{m_{i}}) \leadsto u_{1}(u_{2}( \dots u_{n}(\head{r}))\dots)\]

bibliography:../../all.bib