- From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
- Date: Mon, 22 Apr 2002 12:05:58 +0100
- To: "Pat Hayes" <phayes@ai.uwf.edu>
- Cc: <www-webont-wg@w3.org>
- Message-ID: <JAEBJCLMIFLKLOJGMELDCEMDCDAA.jjc@hplb.hpl.hp.com>

Re: SEM: comprehensive entailments without dark tripleThanks Pat, that was very helpful. I think you are raising two substantive issues (A,B) and one insubstantive one (C) A) KIF has a cheating finiteness assumption with lists B) How do the comprehension axioms work to show equivalence C) I omitted some quantifiers in error. (A) I have no prior experience with KIF and cannot comment on this. (B) How do the comprehension axioms work to show equivalence? Pat: You should put the missing quantifiers in and see what you get. Those two existentials are inside the scope of four universals (quantifying ?x ?y ?lx and ?ly), so the intersection class depends on two classes *and two lists*. So if I make an intersection of classes A B and C using one list to encode (A intersect B) and another one using a different list to encode the same intersection, I now have two distinct intersections. (They would be referred to by different skolem terms if you skolemized the formula.) How will you say that these classes are identical? The desire to have two distinct objects reflecting two distinct syntactic formulations of the same underlying set was deliberate. Very simply examples are: a.. X is the same as unionOf [ X ] is the same as intersectionOf [X] is the same as intersectionOf[ unionOf[ X ] ]. I think the example you pull out is showing that a.. intersectionOf[X,Y] and intersectionOf[Y,X] are the same. Within the overall method of encoding these syntactic structures within the model it is clear that they are "different" and we need to prove that from a semantic point of view that they are the "same". My understanding of the axiomatic approach to DAML+OIL is that this is already there in Fikes&McGuiness's axioms that I am extending to include that these sets exisit. (<=> (PropertyValue intersectionOf ?c1 ?l) (and (Type ?c1 Class) (Type ?l List) (forall (?c) (=> (PropertyValue item ?l ?c) (Type ?c Class))) (forall (?x) (<=> (Type ?x ?c1) (forall (?c2) (=> (PropertyValue item ?l ?c2) (Type ?x ?c2))))))) [intersectionOf axiom 1] appears to be the crucial axiom; I assume that this can be chained together with two specific lists [X,Y] and [Y,X] tp show that intersectionOf[X,Y] and intersectionOf[Y,X] are the same. Do you think that that might not work? I was guessing that we can show that the two intersectionOf classes have the same extension from this axiom; and then we can use the sameClassAs axioms to show that having the same extension entailed being equivalent at some level. We can use the subClassOf axiom (<=> (PropertyValue subClassOf ?csub ?csuper) (and (Type ?csub rdfs:Class) (Type ?csuper rdfs:Class) (forall (?x) (=> (Type ?x ?csub) (Type ?x ?csuper))))) [subClassOf axiom 2] to show that each is a subclassof the other, and then (=> (and (PropertyValue subClassOf ?c1 ?c2) (PropertyValue subClassOf ?c2 ?c1)) (PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs theorem 2] Shows they are the sameClassAs each other. My understanding of the equivalentTo axioms then suggests that we conclude a KIF '=' between the two classes. This means that (after taking "the DAML+OIL with comprehension" closure) each and every class has an infinite number of intersectionOf arcs hanging off it. Personally, I don't like that, but that's my reading of the WG's desires to permit more class entailments. Does this look like enought detail, or do I need to download a KIF reasoner and generate a full proof? Jeremy -----Original Message----- From: Pat Hayes [mailto:phayes@ai.uwf.edu] Sent: 20 April 2002 01:52 To: Jeremy Carroll Cc: www-webont-wg@w3.org Subject: Re: SEM: comprehensive entailments without dark triples I promised I would look at Jeremy's proposed axioms for a 'layerable' version of OWL. Comments below, in-line. Summary: a set of comprehension axioms compatible with the axiomatic semantics for D+O Summary2: Jeremy has another futile effort to persuade a pair of stubborn logicians that the layering problems can be solved without recourse to dark triples. Summary3: a new variant of a first order theory that has the "appropriate entailments" (e.g. the desired intersection really does exist!) Appendix: The comprehension axioms. =================================== (=> (Type ?x rdfs:Class) (exists (?l ?i ?u) (and (Type ?l list) (PropertyValue first ?l ?x) (PropertyValue rest ?l nil) (Type ?i rdfs:Class) (Type ?u rdfs:Class) (PropertyValue intersectionOf ?i ?l) (PropertyValue unionOf ?u ?l)))) i.e the intersection and the union of a single class exist. It is a theorem that these are both equal and equal to ?x. Assuming a KIF function APPEND (=> (and (Type ?x rdfs:Class) (Type ?y rdfs:Class) (Type ?lx list) (Type ?ly list) (PropertyValue intersectionOf ?x ?lx) (PropertyValue intersectionOf ?y ?ly) ) (exists (?z ?lz) (APPEND ?lx ?ly ?lz) % ?lx appended to ?ly makes ?lz (Type ?lz list) (Type ?z rdfs:Class) (PropertyValue intersectionOf ?z ?lz))) i.e. given two intersections with short lists of classes to intersect, we can make a longer list. You should put the missing quantifiers in and see what you get. Those two existentials are inside the scope of four universals (quantifying ?x ?y ?lx and ?ly), so the intersection class depends on two classes *and two lists*. So if I make an intersection of classes A B and C using one list to encode (A intersect B) and another one using a different list to encode the same intersection, I now have two distinct intersections. (They would be referred to by different skolem terms if you skolemized the formula.) How will you say that these classes are identical? BTW, this is one of the layering problems we already have, but appearing in a slightly different form. These definitions get syntactic entities confused with semantic ones, and they get in one another's way. This includes all of Peter's Student Employee cases I think. OK, good. But now we have more work to do. We need to know that if you permute those lists, you get the same intersectionOf and unionOfs. And we need to know that if you have duplicates anywhere in those lists then the intersections and unions are the same as the ones with the duplicates removed, and we need to know the distribution laws (intersecting with a union is unioning the intersections, etc.). You COULD do all that. In effect, you would be taking an implementation of finite sets in LISP, with recursive definitions of all the search and permutation functions, and then transcribing it into KIF axioms. BUt now the OWL reasoner has to actually do all this *as inference*. Or, of course, you could kind of cheat and just write it all out in code, and *pretend* that it was doing all this inference. BUt would you be *sure* that it wasn't missing anything? BTW, I havn't mentioned the fact that these recursions only work in KIF because KIF kind of cheats on its notion of 'list', in effect sneaking in a non-first-order assumption (that all lists are finite) in by the back door. In order to justify this properly you have to assume infinitary rules of inference (for details see http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf) Similarly for union. (=> (and (Type ?x rdfs:Class) (Type ?y rdfs:Class) (Type ?lx list) (Type ?ly list) (PropertyValue unionOf ?x ?lx) (PropertyValue unionOf ?y ?ly) ) (exists (?z ?lz) (APPEND ?lx ?ly ?lz) % ?lx appended to ?ly makes ?lz (Type ?lz list) (Type ?z rdfs:Class) (PropertyValue unionOf ?z ?lz))) Then the other axioms take care of disjointUnion see [disjointUnionOf axiom 1] http://www.w3.org/TR/2001/NOTE-daml+oil-axioms-20011218#5.2.6 oneOf is very similar: (forall (?x) (exists (?l ?o) (and (Type ?l list) (PropertyValue first ?l ?x) (PropertyValue rest ?l nil) (Type ?o rdfs:Class) (PropertyValue oneOf ?o ?l)))) (=> (and (Type ?x rdfs:Class) (Type ?y rdfs:Class) (Type ?lx list) (Type ?ly list) (PropertyValue oneOf ?x ?lx) (PropertyValue oneOf ?y ?ly) ) (exists (?z ?lz) (APPEND ?lx ?ly ?lz) % ?lx appended to ?ly makes ?lz (Type ?lz list) (Type ?z rdfs:Class) (PropertyValue oneOf ?z ?lz))) This is where that KIF cheating comes in. How do you know that this definition works? (What if the list were infinitely long, and the oneOf you were looking for was at a transfinite ordinal? OK, you are assuming that lists are never infinitely long. Can you guarantee that, in all models of these axioms, though? (Not in FOL.)) complementOf is the most straight forward (=> (Type ?x rdfs:class) (exists (?c) (PropertyValue complementOf ?x ?c))) Restrictions are a little different in detail, but similar in intent. % toClass (=> (and (Type ?p Property) (Type ?c rdfs:Class)) (exists (?r) (and (Type ?r Restriction) (PropertyValue onProperty ?r ?p) (PropertyValue toClass ?r ?c) ) ) ) OK, but look: what exactly does this mean? The answer is, it depends entirely on what those quantifers (the ones you havn't bothered to write, that universally quantify over ?p and ?c) range over. All classes and all properties, right? And what is "all" here, exactly? One thing for sure, since KIF isn't higher-order, it does not mean "all" in the mathematical sense. In fact, what it really means is, all the ones that have a name in the Herbrand universe. Do you have a clear idea which ones those are? Also, this says that a restriction *exists*. Where does it say what that *means* ? % hasClass (=> (and (Type ?p Property) (Type ?c rdfs:Class)) (exists (?r) (and (Type ?r Restriction) (PropertyValue onProperty ?r ?p) (PropertyValue hasClass ?r ?c) ) ) ) I guess we may want to combine these, (somewhat ugly): % hasClass & toClass (=> (and (Type ?p Property) (Type ?c1 rdfs:Class) (Type ?c2 rdfs:Class)) (exists (?r) (and (Type ?r Restriction) (PropertyValue onProperty ?r ?p) (PropertyValue hasClass ?r ?c1) (PropertyValue toClass ?r ?c2) ) ) ) % hasValue (forall (?v) (=> (Type ?p Property) (exists (?r) (and (Type ?r Restriction) (PropertyValue onProperty ?r ?p) (PropertyValue hasValue ?v) ) ) ) I omit combining hasValue with toClass, hasClass and hasClass & toClass. % cardinality (=> (and (Type ?p Property) (Type ?i NonNegativeInteger)) NonNegativeInteger isn't first-order definable, either, BTW. (exists (?r) (and (Type ?r Restriction) (PropertyValue onProperty ?r ?p) (PropertyValue cardinality ?r ?i) ) ) ) Similarly for minCardinality, maxCardinality. I find 2^6-1 combinations of properties of restrictions. Some of course are necessarily empty, but still we probably should list the lot. Anyway I will do the worst here (forall (?v) (=> (and (Type ?p Property) (Type ?card NonNegativeInteger) (Type ?min NonNegativeInteger) (Type ?max NonNegativeInteger) (Type ?c1 rdfs:Class) (Type ?c2 rdfs:Class)) (exists (?r) (and (Type ?r Restriction) (PropertyValue onProperty ?r ?p) (PropertyValue minCardinality ?r ?min) (PropertyValue maxCardinality ?r ?max) (PropertyValue cardinality ?r ?card) (PropertyValue hasClass ?r ?c1) (PropertyValue toClass ?r ?c2) ) ) ) ) etc. I won't address the Q ones, since we've dropped them from OWL. I've not looked at them, but guess this method could address them. Pat -- --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes

Received on Monday, 22 April 2002 07:06:35 UTC