- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Thu, 17 Oct 2002 00:11:04 +0200
- To: Ian Horrocks <horrocks@cs.man.ac.uk>
- Cc: Dan Connolly <connolly@w3.org>, Pat Hayes <phayes@ai.uwf.edu>, www-webont-wg@w3.org
On October 16, Ian Horrocks writes: > > 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. direct encoding can indeed be quite useful/performant (we tend to use it for variable predicates) so is it right that you add not(forall ?x C(?x) -> E(?x)) or in other words forsome i C(i) & not(E(i) but you also have E(i) and so you have proven by contradiction ? > 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. I think there is some balance to be found between direct encoding and axiomatization > > > > > 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/ > > -- , Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Wednesday, 16 October 2002 18:11:41 UTC