- From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
- Date: Thu, 18 Apr 2002 09:35:03 +0100
- To: <www-webont-wg@w3.org>

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!) Having made out yesterday that a theory of classes would be a lot of work, I thought again. I had another (well really my first proper) look at the axiomatic semantics for D+O [1]. The axiomatic semantics does not include the ability to infer the existence of an intersection or a union from the existence of a pair of classes. My understanding was the WG would like this. Well, as long as we are content to restrict ourselves to non-self-referential class expressions, this seems really quite straight forward. We can add comprehension axioms to create intersections and unions and oneOfs and restrictions and complementOfs. I give the details below, in an appendix (this is my first ever e-mail with an appendix). What these do not gurantee is that the peculiar self-referential structures exist. A straight-forward ("standard") model of these comprehension axioms could be built out of tree-like expressions that were freely generated from the elements of a model of the original axiomatisation with a syntactic variant for each of the comprehension axioms. e.g. from classes labelled <c1>, <c2> and the numbers 1,3 and the propertys <p1>,<p2> we can generate new classes such as: "complementOf(<c1>)" "intersectionOf([oneOf([c2]),oneOf([c1,c1,c2,oneOf[c1]]))" "restriction(onProperty(p1),minCardinality(3),hasClass(oneOf([c1])))" these new classes as objects in the domain of discourse can simply be strings like the above (somehow distinguished from the xsd:strings that are already in the universe). Their semantics, (the relationship that hold under rdf:type) follows from the axioms. A consistency proof can then be generated from a model for the original (consistent?) axioms augmented by a countably infinite set of these additional classes. Of course, there will be non-standard models that may be a little peculiar, but that's life. I think that this sort of approach will have a number of advantages over dark triples, mainly already given by Fikes and McGuinness: - "The axioms are designed to reflect the layering of RDF, RDF-S, and DAML+OIL" - "designed to place minimal constraints on the interpretation of the non-logical symbols in the resulting logical theory" - " the axioms do not require use of a set theory, that classes be considered to be sets or to be unary relations, nor do they require that properties be considered to be mappings or binary relations." Thus, there is no presumption that RDF is wrong in having antifoundation in its theory of classes. Layering works. Everything is extensibility. Reference ========= [1] Fikes, McGuinness, Axiomatic Semantics for RDF, RDF-S, and DAML+OIL http://www.w3.org/TR/2001/NOTE-daml+oil-axioms-20011218 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. This includes all of Peter's Student Employee cases I think. 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))) 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) ) ) ) % 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)) (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.

Received on Thursday, 18 April 2002 04:36:37 UTC