IFP and datatype properties

A feature of OWL Full that is fairly widely used, but not in DL is the 
ability to declare a datatype property as inverse functional.

I seemed to remember that the reason for excluding it from DL was to do 
with complexity rather than decidability; and that there was a horrocks 
paper on the topic.

I can't find such a paper. Any pointers please?


Also:

Given an ontology A, which would be in DL except that property p is 
declared as both inverse functional and a datatype property, and for 
simplicity, p is not subPropertyOf or equivalentProperty to any other 
property, we can construct an ontology B as follows:

a) replace every triple
         a p d .
    with
         a p' data:d .

b) replace every hasValue d restriction on p, with a hasValue data:d 
restriction on p'.

c) for each data:d1 and data:d2 URIs so introduced with data:d1 != 
data:d2 add
     data:d1 owl:differentFrom data:d2 .

Then B is an OWL DL ontology and is consistent iff A is consistent.

Since B is only polynomially more complex than A, it would seem that 
this is tractable.

Bold assertion: this generalizes to all use of IFP and DP.

Comments?

Jeremy