SEM: comprehensive entailments without dark triples

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