- 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