[Core] 1) editorial things in Core and 2) first draft of Eiter-Schindlauer safety.

When going through the current safeness definition, I
1) had some open quesitions and editorial suggestions and
2) thought it turns out that strong safeness in the Eiter Schindlauer
sense probably "goes quite well" with the definitions Jos set up for safety.

Let's go for 1) first:

"t=?V, in the context of ψ, iff all variables appearing in tare safe
(resp., strongly safe) in ψ', which is obtained from ψ by replacing
every occurrence of ?V=t with And(), in the context of ψ'. "

* I think that ?V=t should be replaced by t=?V, right?

* "(resp., strongly safe)" should be
   "(or strongly safe, resp.)" as far as I know.

* "for every variable symbol ?V and each occurrence of ?V in an atomic
formula α, let χ be the largest subformula of ψ such that α is a
subformula of χ and ?V is strongly safe in χ, then all occurrences of
?V in χ must be replaced with the symbol b; and with u otherwise,"

I don't really understand what the "otherwise" is referring to and where
I should replace ?V with u.

* "Forall ?x ?y ?z ?u (ex:p(?x) :- Or(
   And( ex:q(?z) pred:iri-string(?x ?z)))
   And( ?x=?y ?y=?u ex:q(?u)))"

should be:

Forall ?x ?y ?z ?u (ex:p(?x) :- Or(
   And( ex:q(?z) (External pred:iri-string(?x ?z))))
   And( ?x=?y ?y=?u ex:q(?u)))

What about nested Externals?, I think the b-u replacement needs to be
defined recursively to cater for those, yes? I.e. starting with the
leaves of any nested subformula with externals, you start to apply your
algorithm and, if, there is a valid binding pattern for the formula, one
may replace that formula by b. Does that work?

Now for 2). I probably need jos' help to get that straight, but here a
first attempt to extend the notion of safe rule implications to strong
safety of a ruleset in the sense of Eiter&Schindlauer&Tompits.
To this end, I transcribed my sketch from
to the notation in the Core document. This shall go in place of the
Editor's note

"Editor's Note: The working group has resolved to further extend this
notion of safeness to Eiter-Schindlauer safeness but place this
extended notion at risk. The definition of the additional constraints
which constitute Eiter-Schindlauer safeness and the associated At Risk
note are to be added."

A ruleset consisting of only safe rule implications is called safe.
We now extend this notion to <i>strongly safe rulesets</i>.
The notion of <i>strongly safe</i> rulesets is inspired by
[Eiter&Schindlauer&Tompits] and implies that the ruleset always has a
finite set of ground atomic formulas entailed.
Let r be a set of safe rule implications of the form
<tt>φ :- ψ</tt>
as defined above. Then r<sub>a</sub>, the set of <i>adorned
rules</i> corresponding to r, is obtained as follows:
For each replacement <tt>&theta;</tt> of variable occurrences in <tt>φ 
:- ψ</tt> as defined
before, a rule r<sub><tt>&theta;</tt></sub> is added to r<sub>a</sub>
such that
<li>each variable ?X with ?X/<tt>b</tt> in <tt>&theta;</tt> is replaced by
?X<sub>b</sub>, i.e., we say "?X is adorned with <tt>b</tt> in 
r<sub>&theta;</sub>", and</li>
<li>each variable ?X with ?X/<tt>u</tt> in <tt>&theta;</tt> is replaced by
?X<sub>u</sub>, i.e., we say "?X is adorned with <tt>u</tt> in 

Let R be a ruleset of safe rule implications.
Then, by R<sub>a</sub> we denote &cup;<sub>r in R</sub> r<sub>a</sub>.

In order to define strong safety of R, we first build a dependency
relation <i>Rel</i> between all head and body predicates (ordinary or
external) occurring in rules r in R<sub>a</sub> as follows:

<li> if H occurs in head of a rule r and H in the body of r then add 
(H,B).</li><li> if B occurs in the body of a rule r and H in the head of 
r' such that
   B and H unify, then add (B,H)</li>
<li>if B is an external predicate with ?X adorned with 'u' or an 
ordinary predicate with variable ?X adorned with 'b', and B' is an 
external predicate with ?X adorned with 'b' such that B,B' appear in the 
same rule body, then add (B',B).

We say predicate P depends on Q if (P,Q) is in Rel.  We say P
transitively depends on Q, if (P,Q) is in the transitive closure
<i>Rel<sup>*</sup></i> of <i>Rel</i>.  We say P strictly depends
on Q if (P,Q) in <i>Rel<sup>*</sup></i> but not vice versa.
We are now ready to define strong safety:
Let r be a rule in R<sub>a</sub>. Let further <i>In</i> be the
set of all variables appearing in external predicates the body of r
adorned with 'b', i.e. the union of all "input variables" and
<i>Out</i> be the set of all variables appearing in external
predicates the body of r adorned with 'u', i.e. the union of
all "output variables".
Moreover, let S be the set of body atoms B in r,
such that the head atom of r depends strictly on B.
Let V be the set of all variables that occur in the ordinary atoms in
S plus all variables in <i>Out</i>\cup S. Then, r is strongly safe, iff
all head variables in r appear in the body and additionally <i>In</i>
is a subset of V.
We now say that the ruleset R is strongly safe if all rules r in
R<sub>a</sub> are strongly safe.

Received on Tuesday, 14 April 2009 20:08:53 UTC