Re: OWL semantics

On August 14, Dan Connolly writes:
> 
> On Mon, 2002-08-05 at 15:30, Ian Horrocks wrote:
> > 
> > Dear All,
> > 
> > Having made a plea for the resolution of the semantics issue, I would
> > now like to enter into the argument of what form these semantics should
> > take. 
> > 
> > I have tried to summarise below the arguments in favour of what has
> > become known as the "Patel-Schneider" semantics. I have tried to couch
> > this summary in terms that should be accessible to all members of the
> > WG, and I would appreciate the more technically inclined members
> > cutting me a little slack w.r.t. any minor imprecisions that may have
> > crept in as a result.
> > 
> > 
> > Point 1:
> > 
> > I would like to argue that we should KEEP THE LANGUAGE (and the
> > semantics) SIMPLE. In particular, we should make sure that it is (a
> > subset of) first order logic (FOL). I.e., when we talk about classes
> > we mean 1 place predicates, and when we talk about properties we mean
> > 2 place predicates:
> 
> That's more than saying it's a subset of FOL. RDF is a subset
> of FOL, as demonstrated by the Fikes/McGuinness axiomatization;
> the triple
> 	:subj :pred :obj.
> can be seen as
> 	(PropertyValue subj pred obj)
> 
> 
> You're saying that RDF should fit into FOL in a certain
> constrained way. I don't see why it should, when
> the less constraining way works just fine.

RDF is not a predicate logic, and thus not FOL, or even HOL, because
RDF's version of predicates can appear as the arguments of other
predicates. It is possible to transform RDF syntax into FOL syntax and
axiomatise the result in FOL so that an FOL theorem prover can be used
to compute RDF entailment, but the resulting FOL is NOT the same thing
as the RDF from which you started. Notice, for example, that models of
the resulting FOL theories do not look like the models of the RDF from
which they were derived.

Moreover, the embedding requires that the meaning of the standard
vocabulary (subclass, type, etc) be established by a relatively
complex axiomatisation. This has a number of serious consequences,
which have been discussed in other emails.


> > Jane is a Person just in case our ontology entails
> > Person(Jane), and Jane is the mother of John just in case our ontology
> > entails isMotherOf(Jane,John). If the logic is first order, then the
> > arguments of a predicate must always be either a variable or a
> > constant (such as Jane).
> 
> No, only if RDF properties are mapped to first order predicates.
> That doesn't seem like the natural thing to do, since
> the point of the Semantic Web is to be able to say anything
> about anything, in particular, to talk about properties.

It would be the natural thing to do if RDF were really a sub-language
of FOL. The fact that RDF has ambitions beyond what FOL can do is the
whole point.


> > Another way to look at this is that a model of our ontology consists
> > of a set of objects and a mapping function that maps individual names
> > (constants) to single objects, class names to sets of objects and
> > relation names to sets of pairs of objects. Jane is a Person just in
> > case that, in all models of our ontology, the object that Jane maps to
> > is a member of the set that Person maps to, and Jane is the mother of
> > John just in case that, in all models of our ontology, the pair of
> > objects that Jane and John map to is a member of the set that
> > isMotherOf maps to.
> > 
> > That is really all there is to it: you can explain it to pretty much
> > anyone.
> 
> It seems no more difficult to explain with one level of indirection
> between classes/properties and their extensions.

Yes, and FOL is no more difficult to explain than zero-order predicate
logic - we just add variables and a couple of quantifiers.


> > Moreover, it is part of the core curriculum of most
> > undergraduate computer science and maths courses, and many of the
> > people who will be involved in implementing the semantic web will
> > already be very familiar with it. Can we say the same thing about
> > solipsistic logic?
> 
> Non-sequitor: comprehension axioms are orthogonal to the mapping
> of RDF into FOL.

Not at all.  Comprehension axioms are only needed in OWL under a
transformation that maps RDF properties (and OWL restrictions) into
FOL individuals, not when RDF properties are treated more naturally as
predicates.


> > How many of us had ever heard of it before joining
> > the WG, or even now have the slightest idea as to what it is all about?
> 
> I think we knew it as datalog; i.e. eliminating functional
> terms or leaving existentially quantified variables out of the
> conclusion. 
> 
> 
> > Point 1a:
> > 
> > While it is clear that, in some cases, it is useful to be able to talk
> > about classes as instances, we should be clear that this means going
> > outside first order logic into higher order logic (HOL), because we
> > can now have predicates as the arguments of other predicates.
> 
> Not so...

Actually having predicates as the arguments of other predicates takes
us outside even HOL.  Being able to axiomatise the result in FOL or
even zero-order logic doesn't change this.  Many versions of modal
logics can be transformed into FOL and axiomatized, this does *not*
make them FOL, however.


> > If we
> > accept classes as instances, then even OWL Lite (which is supposed to
> > be "viewed by tool builders to be easy enough and useful enough to
> > support") will be a HOL. Some people will argue that it isn't really
> > higher order, but what they mean is that it may be possible (depending
> > on the assumed semantics of the HOL syntax) to embed the HOL in FOL by
> > axiomatising the HOL itself and the HOL ontology in FOL. Imagine this
> > conversation with a potential OWL tool builder:
> > 
> > Tool builder: OWL (Lite) is a higher order logic, so I will need a HOL
> > reasoner, right?
> > 
> > OWL guru: No, no. All you have to do is take a FOL reasoner, an
> > axiomatisation of OWL in FOL, and feed the axiomatisation, plus your
> > axiomatised ontology, into the FOL prover. Piece of cake really.
> 
> Yes, a piece of cake. Several systems already work this way.

And which systems might these be?

It is hard to believe that tool builders will be too impressed to hear
that not only do they need FOL reasoners in their applications, but
that they need to reason about ontologies w.r.t. relatively complex
axiomatisations of the language in which they are written. This
approach simply wont work in practice.


> 
> > It is worth noting that real HOL systems, e.g., Isabelle [1] and HOL
> > [2], don't work via FOL axiomatisation as it is well known that, in
> > practice, you wont be able to prove anything this way.
> > 
> > It is also worth pointing out that such axiomatisations are invariably
> > large and complex, and that it is difficult/impossible to be sure that
> > they are correct. E.g., take a look at the axiomatisation of
> > DAML+OIL/RDF in [3], which contains around 140 axioms. FOL reasoners
> > can be used to detect "obvious" inconsistencies (as happened with
> > earlier versions of [3]), but simply ironing these out is a LONG way
> > from proving that the axiomatisation correctly captures the meaning of
> > the language.
> 
> But with axiomatizations, at least you *can* use automated checking
> techniques, regression testing, etc. This is much better than
> just manually poring over the prose of a model theory, no?

In the end it all comes down to poring over a theory. How else do you
think FOL itself was devised? Our faith in basic logical theories is
grounded on their having been pored over by lots of smart people over
a long period. The beauty of standard MTs like the one proposed by
Peter for OWL is that they are very simple and well understood, the
basic theory having been subjected to just such a scrutiny, and they
are relatively easy for logicians to check.

In contrast, axiomatisations tend to be large, complex and difficult
to understand (individual axioms may seem straightforward, but the
interactions between axioms are not). Automated checking can only
detect (some) basic errors and inconsistencies. This doesn't tell us
much about the meaning captured in the axiomatisation.

The DAML+OIL axiomatisation which you mentioned above is a fine
example of this problem. Peter has shown that it is IMPOSSIBLE to
extend RDF with DAML+OIL while retaining standard entailments. Yet
this is exactly what the DAML+OIL axiomatisation seems to be giving
us. Clearly there is some deep seated problem with the axiomatisation,
but nobody noticed it. Even now, it isn't clear where that problem is
lurking or how to fix it.


> > Point 1b:
> > 
> > It should NOT be possible to use OWL/RDF statements to constrain the
> > meaning of OWL/RDF syntax. E.g., if myTransitive is a sub-class of
> > transitiveProperty, then instances of myTransitive should NOT be
> > treated by OWL as transitive properties.
> 
> But TransitiveProperty isn't -- or: shound not be, IMO -- syntax.
> It's a term just like any other term; subclassing should work
> just fine.
> 
> > If we go down this road, then
> > we need a (HOL) reasoner even to parse the syntax of an OWL ontology,
> > to determine what is being said, and to check that it is valid OWL.
> 
> No, parsing is easy. RDF parsers are cheap and plentiful.
> I'm not sure how hard checking consistency will be,
> nor how important it is that implementations do so completely.
>
> > For example, when we parse an OWL ontology we may find that instead of
> > using the familiar subClassOf property, it contains lots of statements
> > like "Person foo Animal". If we allow statements in the ontology to
> > constrain the meaning of the syntax, then we may be able do deduce
> > that foo is equivalent to subClassOf, and that this is therefore a
> > meaningful OWL statement. The reasoning required for this deduction
> > may be extremely complex. It may even be IMPOSSIBLE to be sure that we
> > have derived the complete syntactic meaning of an OWL ontology
> > (because the language is undecidable).
> 
> This isn't "syntactic meaning." It's just meaning.
> 
> > Another example. In OWL, transitive properties cannot be used in
> > cardinality restrictions. If we allow inference to be used to deduce
> > that a property is a transitive property, then when we parse an OWL
> > ontology we can't be sure that it is valid
> 
> There's that word again; I know what "valid inference" is, I think;
> but I don't know what "valid ontology" is. I think you mean
> something like well-formed formula; but it's easy to tell if
> the formula is well-formed; RDF parsers do that for free.
> 
> > until we have checked that
> > none of the properties used in cardinality constraints can be deduced
> > to be transitive. Again, the required reasoning may be very complex,
> > and it may even be IMPOSSIBLE to be sure that the ontology is
> > syntactically valid.
> 
> There it is again.
> 
> > One can easily imagine situations where the
> > inference that a property is transitive depends on a cardinality
> > restriction involving the property itself, which then becomes a
> > syntactically invalid statement, so the inference is no longer valid
> > (a paradox).
> 
> Hmm... "easily" is relative, I suppose. That looks like an interesting
> test case. Care to spell it out in a bit more detail?
> 
> 
> > To return again to our poor benighted tool builder, can you imagine
> > the reaction we will get when we try to explain that it is impossible
> > to parse an OWL ontology and check it for syntactic validity without
> > employing the services of a (possibly higher order) reasoner?
> 
> That's why we should tell him that an OWL parser is just an
> RDF parser, for which there are lots of implementations and
> a pretty good test suite.

The above points are just a reiteration of the old RDF uber alles
argument which you cling to in spite of the fact that it has been
demonstrated to be incompatible with the way logics work.

OWL extends RDF by giving special meaning to some syntactic
constructions - you would probably say sets of triples, but of course
they only have an OWL meaning when they are in a particular
relationship to each other. Unfortunately, the resulting OWL meaning
could disturb that relationship. For example, what happens if I have
OWL statements that say something like "(A or not A) implies (first =
rest)". This looks like well formed OWL, but if I give it its OWL
meaning, then the list used in the disjunction becomes ill formed.


> 
> > Point 2:
> > 
> > If we decide to go with some form of higher order logic and/or allow
> > reasoning about syntax, then all our efforts to design OWL so as to be
> > relatively simple, and hopefully even implementable, are a (bad)
> > joke. Even the so called Lite version of OWL would be impossibly
> > complex to deal with, as I hope I showed in some of the above
> > examples.
> 
> All you've shown is that you don't like the design. It's quite
> straightforward to work with, as demonstrated by cwm and Euler,
> and a number of integrations with things like prolog, jess,
> etc.
> 
>   http://www.w3.org/2002/03owlt/ontAx.n3
>   http://www.agfa.com/w3c/euler/owl-rules

I presume these are the systems you referred to above.

Of course it is perfectly possible to write some software that does
something. Being clear about exactly what it is doing is another
thing.  I have not seen any comprehensible description of what the
above software does.

Ian and Peter 

> 
> 
> 
> > I guess that is enough to be going on with.
> > 
> > Regards, Ian
> > 
> > 
> > [1] http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html
> > [2] http://www.cl.cam.ac.uk/Research/HVG/FTP/FTP.html
> > [3] http://www.w3.org/TR/daml+oil-axioms
> -- 
> Dan Connolly, W3C http://www.w3.org/People/Connolly/
> 
>

Received on Thursday, 15 August 2002 09:07:17 UTC