- From: Pat Hayes <phayes@ai.uwf.edu>
- Date: Fri, 19 Apr 2002 19:51:59 -0500
- To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
- Cc: www-webont-wg@w3.org
- Message-Id: <p05101551b8e6642d5329@[65.217.30.94]>
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 Friday, 19 April 2002 20:52:10 UTC