OWL semantics

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: 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).

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. 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? 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?



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. 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.

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.


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. 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.

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).

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 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. 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).

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?


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.



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

Received on Monday, 5 August 2002 16:33:02 UTC