Re: OWL semantics

On Thu, 2002-08-15 at 08:04, Ian Horrocks wrote:
> 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.

No, if you look at RDF as FOL, there is only one predicate:
PropertyValue. It can't appear as an argument of other
predicates.

> It is possible to transform RDF syntax into FOL syntax

By 'FOL syntax' you mean an abstract syntax, right? not
any particular ASCII/Unicode syntax.

Well, then RDF is quite a reasonable concrete
syntax for (a subset of) FOL abstract 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.

Yes, it is.

> Notice, for example, that models of
> the resulting FOL theories do not look like the models of the RDF from
> which they were derived.

Yes, they do.

It's pretty arbitrary whether you use the Hayes/Menzel indirection
trick or the Fikes/McGuiness (PropertyValue ...) trick to relate
RDF syntax to first order logic. The models are isomorphic.

If people are getting confused by the Hayes/Menzel indirection
trick, perhaps the LBase stuff is more important than I thought.


> Moreover, the embedding requires that the meaning of the standard
> vocabulary (subclass, type, etc) be established by a relatively
> complex axiomatisation.

This is complex?

  4.2 RDFS-entailment and RDFS closures
  http://www.w3.org/TR/rdf-mt/#rdfs_entail

There are 10 axioms, each of which is a very simple horn clause.

> This has a number of serious consequences,
> which have been discussed in other emails.

I don't recall any consequences about the complexity
of the axiomatization of subclass, type, etc.


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

It is.

> The fact that RDF has ambitions beyond what FOL can do is the
> whole point.

I don't see this point at all.

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

Yes, quite.


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

Hmm... I suppose I see your point.
It seems very unnatural, to me, to treat RDF properties
as FOL predicates, but I don't suppose the '98 specs
completely ruled that out. I thought that having stuff
like properties of classes, e.g.
	rdfs:Class rdfs:label "Class".
ruled that out. But I suppose as long as no interactions
between class membership and other properties were
specified, one could take other approaches.

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

But RDF doesn't have FOL predicates as arguments of other
FOL predicates. It has RDF properties as arguments
of the one PropertyValue FOL predicate.

>  Being able to axiomatise the result in FOL or
> even zero-order logic doesn't change this.

It's not axiomatization that relates RDF syntax to FOL syntax;
it's just the normal concrete-syntax-to-abstract-syntax relationship.

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

"relatively complex?" We're talking about 10 horn clauses, for RDFS.
For OWL, I expect more like 50, but still, hardly a monument
to engineering.

And I expect they won't need a FOL reasoner for most applications.
Jos and cwm are more like pure-prolog engines (with something
like tabling to deal with loops, but with no negation mechanisms)
than FOL reasoners.


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

I hope it comes down to more than just eyeballs poring over a theory.
I hope we can use software engnineering techniques like regression
testing, and like mapping (by machine) our axioms to existing
systems, and such.

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

Hmm... I suppose I have to take your word for that.

But keep in mind that logicians are not the judges of the
success of our language; web developers are.
I think I know more about logic than most web developers,
and I don't find MTs like the one proposed
by Peter very simple at all.

The RDF Core WG has spent the last year or so figuring out
what it takes to explain stuff like model theory to
a bunch of Java hackers. The review feedback I'm getting
says they're starting to get it. I'd really like to
build on that success when explaining OWL semantics to
this crowd.
 

> In contrast, axiomatisations tend to be large, complex and difficult
> to understand (individual axioms may seem straightforward, but the
> interactions between axioms are not).

Surely you don't mean that as a matter of fact, do you?
The RDFS axiomatization is not large; it's 10 horn clauses.

I find axiomatizations much, much easier to understand than
model theories. Many of the folks I collaborate with
agree.

> Automated checking can only
> detect (some) basic errors and inconsistencies.

Yes, automated techniques are limited.

Axiomatizatoins look a lot like programs. Programmers
understand that there are complex interactions between
the lines of a program, and they understand that
the compiler won't tell them that they have zero
bugs in their program, but they like the
fact that the compiler finds syntax and typecheck errors,
and they like syntax coloring tools and lint
and call graph analysis tools and the rest of
the stuff you get from formal artifacts about
a design.



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

No, he has not. He has shown that it is POSSIBLE to extend
it in ways that produce paradoxes.

> Yet
> this is exactly what the DAML+OIL axiomatisation seems to be giving
> us.

If you measure "seems to be giving us" by the way people understand
and use DAML+OIL, then the DAML+OIL model theory seems to be
giving us stuff that it isn't giving us too, like classes
as instances, the ability to use TransitiveProperty as the
range of a property, etc.


> Clearly there is some deep seated problem with the axiomatisation,
> but nobody noticed it.

Yes, we did notice it. In just a few months.

> 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

No, it is not.

> which you cling to in spite of the fact that it has been
> demonstrated to be incompatible with the way logics work.

You mean "the way I(Ian) prefer that logics work", no?

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

No, you just get a contradiction.


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

Hmm... I went to great trouble to explain the design in
the style that you're used to reading:

 http://lists.w3.org/Archives/Public/www-webont-wg/2002Jun/0208.html

In today's telcon, you were willing to admit it as a proposal.

> 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/
> > 
> > 
-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Thursday, 15 August 2002 14:13:11 UTC