W3C home > Mailing lists > Public > www-webont-wg@w3.org > April 2002

Re: SEM: comprehensive entailments without dark triples

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

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:49 GMT