Re: Possible semantic bugs concerning domain and range

On October 16, Dan Connolly writes:
> 
> On Wed, 2002-10-16 at 13:00, Ian Horrocks wrote:
> > On October 16, Dan Connolly writes:
> > > 
> > > On Tue, 2002-10-15 at 16:47, Jos De_Roo wrote:
> > > > 
> > > > >> >>  Range(P, A) -> (forall x,y P(x,y) -> A(y) )
> > > > >> >>
> > > > >> >>  You want
> > > > >> >>
> > > > >> >>  Range(P,A) <-> (forall x,y P(x,y) -> A(y) )
> > > > >> >>
> > > > >> >>  They are about equally clear and intuitive; but the latter rules out
> > > > >> >>  some possibilities which the former permits. I believe that all the
> > > > >> >>  'intuitive' entailments that people want in fact hold in both these
> > > > >> >>  cases; and that the former is therefore to be preferred.
> > > > >> >
> > > > >> >I am agnostic about which of these is to be preferred - as a humble
> > > > >> >engineer, all I need to know is which one it is so that I have a clear
> > > > >> >spec to which I can build my systems.
> > > > >
> > > > >I'm kinda agnostic too... I was leaning toward the IF, rather
> > > > >than the IFF...
> > > > 
> > > > I'm not agnostic at all...
> > > > i.e. I can't see how to write
> > > >   (forall x,y P(x,y) -> A(y)) -> Range(P,A)
> > > > in Horn-clauses or in Datalog
> > > > (although I like nested implications
> > > > in propositional proof arguments)
> > > 
> > > Oohh; that's quite compelling... currently, you can
> > > implement a complete RDFS reasoner with a
> > > horn/datalog reasoner. If we changed range to IFF,
> > > it's not clear that this property would hold.
> > > 
> > > Likewise for subClassOf.
> > 
> > If you use a direct encoding such as the one Benjamin and I have been
> > suggesting (i.e., classes as unary predicates, properties as binary
> > predicates),
> 
> I don't see how that's relevant; if a test for C(i) -> D(i)
> would work, then so would a test for
> 	holds(rdf:type, C, i) -> holds(rdf:type, D, i)

Not unless you axiomatised the interaction between type and
subClassOf. The whole point of the direct encoding is that subClassOf
corresponds to implication, and you can let the logical machinery do
the work for you - which is what it is designed for.

E.g., if my Ontology says that C is a subClassOf D and that D is a
subClassOf E, I add the rules C(?x) -> D(?x) and D(?x) -> E(?x) to my
rule base. Now to check if C is a subClassOf E I can just add the fact
C(i) to my rule base and check if E(i) is entailed by the rule
base. In contrast, if I have the rules holds(rdf:subClassOf,C,D) and
holds(rdf:subClassOf,D,E), then adding holds(rdf:type,C,i) would not
entail holds(rdf:type,E,i) unless I add rule(s) that axiomatise the
relationship between type and subClassOf.

> 
> > then you can check if subClassOf(C,D) holds simply by
> > inventing a new individual i and checking if C(i) -> D(i) holds.
> 
> But in any case, how can I encode that as a horn clause?
> 
> 	subClassOf(C, D) :- ... what to put here? ...

See above: I don't do this at all, I just check if C(x) entails D(x).

Ian

> 
> 
> > Similarly for Range(P,A), you can invent two new individuals i1 and i2
> > and check if P(i1,i2) -> A(i2) holds.
> > 
> > Ian
> 
> -- 
> Dan Connolly, W3C http://www.w3.org/People/Connolly/
>

Received on Wednesday, 16 October 2002 15:49:48 UTC