W3C home > Mailing lists > Public > www-webont-wg@w3.org > August 2002

Re: OWL semantics

From: Leo Obrst <lobrst@mitre.org>
Date: Tue, 06 Aug 2002 17:10:26 -0400
Message-ID: <3D503B42.D0D8D6B1@mitre.org>
To: Ian Horrocks <horrocks@cs.man.ac.uk>
CC: www-webont-wg@w3.org

Ian,

I think you are definitely on-target here. Mostly we have obscured many of
the logical and formal issues, which you make clear.

Leo

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

--
_____________________________________________
Dr. Leo Obrst  The MITRE Corporation
mailto:lobrst@mitre.org Intelligent Information Management/Exploitation
Voice: 703-883-6770 7515 Colshire Drive, M/S W640
Fax: 703-883-1379       McLean, VA 22102-7508, USA
Received on Tuesday, 6 August 2002 17:10:49 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:51 GMT