int/float disjointness

We agreed at F2F 12 to have the value spaces of numeric types be
disjoint [1], so that numeric builtins could use the normal math
libraries.  We implicitely agreed to Dave's three test cases:

> RS1: [3]
>    ex:a = "1"^^xsd:double
>    ex:p(?x) :- ?x = External(func:numeric-add(ex:a,
>                                   "0.0000000001"^^xsd:double))
> entails:
>    ex:p("1.0000000001"^^xsd:double)
> 
> but:
> 
> RS2:
>    ex:a = "10000000"^^xsd:double
>    ex:p(?x) :- ?x = External(func:numeric-add(ex:a,
>                                   "0.0000000001"^^xsd:double))
> entails:
>    ex:p("10000000"^^xsd:double)
> 
> what's more the XPath type promotion rules mean that:
> 
> RS3:
>    ex:a = "10000000"^^xsd:double
>    ex:p(?x) :- ?x = External(func:numeric-add(ex:a,
>                                   "0.0000000001"^^xsd:decimal))
> also entails:
>    ex:p("10000000"^^xsd:double)

Now, in thinking about talking to OWL-WG about this, I'm wondering about
a few other test cases.  In particular, I think in RIF Core, for the
empty ruleset:

   "1"^^xsd:decimal = "1"^^double    IS NOT entailed

but

   pred:numeric-equal("1"^^xsd:decimal, "1"^^double)  IS entailed
   
Agreed?

The question then, for OWL, is whether it's possible to still have

   "1"^^xsd:decimal owl:sameAs "1"^^double.   

be entailed.  Can we still allow that?  I think we could implement it in
OWL-RL, using datatype guards and builtins, as above.

I'm trying to figure out whether our "push back" on OWL on this subject
actually changes their implementations, or is really just about how they
conceptualize the language.

      -- Sandro

[1] http://www.w3.org/2005/rules/wg/meeting/2009-01-15#resolution_10