[SCL] Some questions for SCL and RDF
pat hayes
phayes at ai.uwf.edu
Mon May 12 18:03:18 CDT 2003
>Hi,
>
>After brief thinking about SCL and RDF relations
>some questions came up. I'd appreciate a lot
>if you can shed some light on the issue described below.
Yes, this is a central issue in what might be called the RDF family
of languages. One can classify various people in the WGs by their
attitude to this issue.
>Let us take a file in RDF or OWL. Pat has a nice
>semantics for this (both the mainstream one and
>the one in http://www.coginst.uwf.edu/~phayes/OWL2LBASE.html).
>I have also seen alternative semantics (possibly
>partial) along the same lines.
>
>The machinery used in these semantics is
>explicit encoding. RDF and OWL formulas are
>not translated "directly" to FOL. Instead,
>a number of predicates like type, class,
>relation, symmetric etc are used.
Well, it is not clear that the use of these involves 'indirection'.
They are after all first-class RDF and RDFS and OWL relations in
their own right, and under the very same 'direct' translation they
also map into CL relations. Whether or not to view this 'auxiliary'
vocabulary as first-class seems to be a matter of taste. My own view
is that it is semantically more transparent to do so, in particular
to express rdf:type (the relationship between an entity and a
predicate (/class) which is true of it) as itself a binary relation:
rdf:type(?x,?) iff ?y(?x)
which is perfectly fine SCL. One of the great merits of SCL over
traditional FOL syntax is that it allows one to write things like
this without subterfuge.
>These predicates are associated with a finite
>list of axioms.
There are some axioms, indeed, which encode the 'semantic
assumptions' associated with the RDFS and OWL vocabularies. Most of
them are clearly definitional in nature, however.
>Now, if you take a naive understanding of an
>RDF or Owl formula, you would not use the
>predicates class, type, etc directly.
I disagree. Again, this is a matter of style. One can - I speak from
experience here - get quite used to expressing oneself in terms of
classes and properties, and the use of these predicates is then quite
natural; and some of them map into quite natural relations even in a
more conventional logic, eg rdf:Class is precisely the property of
being a unary relation, which is a very handy property for many
applications. It is true that, coming from a FOL world, one would not
naturally use the equivalent of rdf:type as a binary predicate, but
this way of thinking of predicates as 'types' is itself suggestive
and is found very intuitive by many users.
>If "man" is a class and "human" is a class
>and one is a subclass of another you'd like
>to say "forall x . man(x) implies human(x)".
>
>The standard semantics machinery does not
>take this route.
It takes a slightly longer route to the same place: it just
introduces "subClass" as a property in its own right, with the
obvious connecting axiom
subClass(?x ?y) iff forall ?z (?x(?z) implies ?y(?z) )
and then translates - transcribes would be better - rdfs:subClassOf
into subClass. The 'direct' translation then become simply a matter
of replacing this by its definition, as one could reasonably call it.
It all 'normal' cases this works directly; it has the additional
merit of allowing a translation of many RDFS/OWL theorems which would
not get translated at all in the other style of translation, eg the
fact that rdfs:subClassOf is in the class owl:TransitiveProperty,
which goes by the following route, starting with an OWL-valid RDF
triple:
rdfs:subClassOf rdf:type owl:TransitiveProperty .
-->
type(subClass, TransitiveProperty)
<=>
TransitiveProperty(subClass) eliminate type
<=>
(subClass(?x ?y) and subClass(?y,?z)) implies subClass(?x ?z) eliminate TP
<=>
(forall ?u (?x(?u) implies ?y(?u) ) and (forall ?u (?y(?u) implies ?z(?u))
implies (forall ?u (?x(?u) implies ?z(?u) ) eliminate subClass
which of course is a logical truth, as required. It is important to
some applications of SCL in the SW effort that derivations like this
are possible.
>Now, I do understand the
>encoding machinery, which is fairly
>classical (we could always just use one
>predicate "apply" and encode any intuitive
>predicate as a constant, for example).
>
>For example, combinatory logic is built up like
>the RDF/OWL semantics machinery.
>
>For the SCL-RDF connection I'd be much
>happier with a more direct conversion
>machinery, where you would translate the
>fact that man is a subclass human like
>"forall x . man(x) implies human(x)".
I would not, because this would not be a complete embedding of RDF
into CL. A great deal of effort has been predicated on the use of
RDF-style encodings, and it would be foolish for us to define a
mapping which was incompatible with this effort.
HOwever, I think we can define BOTH, in fact, and explain what their
respective advantages are. And then the interesting task left is to
state claenly and precisely what the exact relationship between them
is. If D is the 'direct' one that you prefer, and T is the
transcription, and A the relevant axioms, then clearly T+A entails D
wherever D is defined; but we can surely do better than this. What
ought to be true is that for any E with the same signature as D, T+A
entails E iff D entails E.
>
>There are several reasons for this:
>
>- such a translation would be naturally
>combinable with ordinary, non-RDF/non-OWL FOL.
So would the longer mapping via the OWL/RDF-named relations.
>
>- such a translation is much much better for
>automated theorem proving. Before attempting
>to answer queries from RDF/OWL I'd surely do
>whatever possible to convert the meanings
>directly, without using the extra axioms.
That may well be true, but I think that can be handled separately.
For example, it would make very good pragmatic sense to postprocess
any such translation into CL from OWL or RDFS by expanding out all
iff definitional axioms involving the OWL or RDFS vocabularies as far
as possible. But it would also make sense to do other special
processings as well, eg on things like the ugly OWL lists used in the
owl:oneOf and owl:intersectionOf constructions.
>Any encoding layers are typically a real
>horror for a prover. You do want to eliminate
>the encoding layers as much as possible.
Quite, but there are other reasons for wanting a complete
translation, eg the use of CL as a semantic reference language (which
I anticipate will be its most important SW use in the near term.) So
let us do both. Defining the translations is pretty easy, and it is
easier to discuss their relationships inside SCL than in terms of
mappings from RDF/OWL.
>Also, observe that a formula F and an encoded formula enc(F)
>are typically not equivalent, since the signatures
>of F and enc(F) are different (analogy to Skolemisation:
>Skolemised formula sk(F) is not logically equivalent
>to a non-Skolemised formula F, although their
>consistencies are equivalent: one is consistent
>iff another one is).
Right, and the best way to define the 'reduction' might be in terms
of a 'weakly equivalent' theory with a non-OWL/RDF signature. I need
to work on this in any case, so lets try to get it clear. See above.
>
>For the practical purposes of combining SCL
>and RDF/OWL it would be IMHO nice to have
>a translation machinery RDF/OWL->FOL which
>does not rely on axioms being added to
>the output of the translation.
>
>Has anybody worked on such a translation
>(IMHO a necessity for FOL theorem proving in
>the Owl context)?
Not adequately. But I agree it is worth doing, and plan to do it as
part of this work.
>Even if it may be hard for the general case,
>surely we can translate large subsets of RDF/OWL
>in the direct manner.
I think we can certainly do it for OWL-DL but in fact also for rather
more of OWL. What cannot be so translated is applications of the OWL
constructions to the OWL vocabulary itself, eg an owl:restriction on
rdf:type, for example. Sometimes such things have obviously silly
consequences in any case, but some of them are in fact quite
meaningful.
What worries me more is how to give an adequate FOL or CL
translation for the cardinality restrictions in OWL. These map
naturally into numerical quantifiers.
Does anyone want us to allow numerical quantifiers in SCL syntax ???
Pat
--
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32501 (850)291 0667 cell
phayes at ai.uwf.edu http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu for spam
More information about the Scl
mailing list