Re: Issue-31: Disjoint sorts - sketch of test case

<snip/>

> ** ONDS to DS
> 
> The source rule uses the same identifier for distinct objects so the
> translator needs to introduce new identifiers:
> 
>   Forall ( p_unary_pred(a) :- And())
>   Forall ( q_unary_pref(b) :- And())
>   Forall ( p_individual = q_individual :- And())
> 
> Query: p_unary_pred(?x)
> 
> The translation is straightforward but the form of identifiers in the
> target system may not be intuitive.
> 
> A static analyis could omit the identifier renaming for constants
> which are not subject to punning but that leads to a non-monotonic
> translation which is undesirable (at least in the OWL setting).
> 
> ** ONDS to OS
> 
> Same as for ONDS to DS, the translator has to introduce new
> identifiers.

No, this would not work.

Say you have a rule and a fact:

Forall x,y (x=y).
p(a).

Under ONDS, this entails p(a), but not q(a).
Under OS, this entails both p(a) and q(a).

You can rename your symbols as much as you want, but every symbol will
be interpreted as the same symbol.

Conclusion: translations from DS and ONDS to OS do not work in the
general case.


Best, Jos

> 
> ** OS to DS
> 
> Hummm ...
> 
> If we can assume an equality operator for predicates (=pred=) then I
> guess the translation would be something like:
> 
>   Forall ( p_unary_pred(a) :- And())
>   Forall ( q_unary_pref(b) :- And())
>   Forall ( p_individual =indivdual= q_individual :- And())
>   Forall ( p_unary_pred =pred= q_unary_pred)
> 
> Query: p_unary_pred(?x)
> 
> If not then we would have to rewrite all of the rules involving p and q
> to introduce the alias syntactically:
> 
>   Forall ( p_unary_pred(a) :- And())
>   Forall ( q_unary_pref(a) :- And())
>   Forall ( p_unary_pred(b) :- And())
>   Forall ( q_unary_pref(b) :- And())
>   Forall ( p_individual = q_individual :- And())
> 
> Query: p_unary_pred(?x)
> 
> ** OS to ONDS
> 
> Would be either:
> 
>   Forall ( p(a) :- And())
>   Forall ( q(b) :- And())
>   Forall ( p =indivdual= q :- And())
>   Forall ( p =pred= q :- And())
> 
> Query: p(?x)
> 
> or
> 
>   Forall ( p(a) :- And())
>   Forall ( q(a) :- And())
>   Forall ( p(b) :- And())
>   Forall ( q(b) :- And())
>   Forall ( p = q :- And())
> 
> Query: p(?x)
> 
> Dave
> 
> [1] http://www.w3.org/2005/rules/wg/wiki/Issue-31
>

Received on Tuesday, 1 May 2007 16:37:27 UTC