Re: OWL semantics

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.

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


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

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

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

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

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


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

> 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 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 Wednesday, 14 August 2002 13:36:22 UTC