Re: OWL semantics

On August 6, Christopher Welty writes:
> 
> WIth regards to Ians two basic points:
> 
> 1a) Classes as instances:
> 
> This is, to me, a fascinating issue, and I'm not willing to take Ian and 
> Peter's word on it yet.  It is certainly a useful feature to have.  Pat 
> and Chris Menzel worked out a way to make the semantics of this 
> first-order for KIF/CL/whatever it's called now, however to my knowledge 
> they have never shown any of the (algorithmic) consequences for reasoning. 
>  Pat shrugs and says it should be no problem since it's all first order, 
> and the syntax prevents paradoxes.  I'm not willing to take their word for 
> it, either.

Allowing classes of classes cannot be done directly in standard first-order
logic while retaining a natural correspondence between classes and
predicates.  Either changes have to be made to first-order logic, perhaps
in the way proposed by Pat Hayes and Chris Menzel, or the instance-class
relationship has to be some other relationship than membership in the
extension of a predicate.  

These changes do not, however, come for free.

The first change requires the development of a different logic.  Pat Hayes and
Chris Menzel have embarked on this path, but with a different logic comes
the possibility of changes in the characteristics of the logic as well as 
requirements for different tools to work with the logic.

The second change interferes with the natural embedding of OWL into FOL, an
embedding that provides considerable benefits.  In other words, instead of
OWL really being a portion of FOL, OWL would be a language whose meaning we
could describe using FOL.

Some of the consequences of losing a natural embedding are that:

1. Instead of OWL mapping directly to a fragment of FOL with relatively
nice computational properties, the meaning of OWL would be described using
(at least) full FOL.

2. Instead of relying on the built in machinery of FOL to deal with
intersection, union, negation, etc., it would be necessary to treat them as
standard predicates whose meaning is described by the axiomatisation.

As we have already discussed, it is not easy to be sure that the
axiomatisation correctly captures the meaning of the language. Moreover,
even if we believe that it is correct, using the axiomatisation can be very
costly form a computational perspective: instead of reasoning directly with
boolean connectives, for example, we have to reason with an axiomatisation
of their meaning. Many of the optimisations built into existing FOL
reasoners would be rendered ineffective as they would not be able to
recognise and exploit the properties of the axiomatised connectives.


> Applying this result (assuming there is an algorithm) to OWL may not be 
> trivial, however, since much computation in description logics occurs over 
> the class descriptions - even if it the reasoner is model based.  So, at 
> least from what I understand, a lot hinges on the fact that the extension 
> of a class does not include other classes.  Still, what are the 
> consequences of including classes in the extension of classes?  An 
> inference may add more to the description of a class?  As long as that 
> addition is monotonic, is it really that bad?
> 
> So Ian, Peter, are you objecting prima facie to the fact that "classes of 
> classes" is inherently second order, or do you have examples in mind that 
> would break the reasoner?

I have no idea how to build a "direct" reasoner for such a language (I
could, of course, use the axiomatisation approach), so I can't say how
such a reasoner might be broken. The fact that inferences are
monotonic doesn't really help much - we have to be sure that we are
adding all and only correct inferences, and that we are not going to
add infinitely many inferences.

Regards, Ian


> 
> 1b) Using OWL to change the syntax of OWL
> 
> I strongly agree with Ian's position here.   It is well known that when 
> you use a logical system to *talk about itself* you are introducing 
> incompleteness.  This was part of Godel's theorem.  In every system that 
> permitted this I've ever seen, it was a trivial matter to create 
> incomplete and infinite proofs, so trivial that naive users did it all the 
> time.  Unless you break processing into two discrete steps, the way 
> compilers/loaders do (i.e. compile time and run time) you are also 
> introducing a huge amount of machinery to support this.  Machinery that no 
> one really knows how to build. 
> 
> Adding such a class of  features reduces the space of possible 
> implementors for the full language from a handful to none.  It may be 
> interesting to create that as "OWL level three" and make it a challenge 
> problem for Computer Science.
> 
> -ChrisW
> 
> 
> Dr. Christopher A. Welty, Knowledge Structures Group
> IBM Watson Research Center, 19 Skyline Dr.
> Hawthorne, NY  10532     USA 
> Voice: +1 914.784.7055,  IBM T/L: 863.7055
> Fax: +1 914.784.6078, Email: welty@us.ibm.com

Received on Thursday, 8 August 2002 09:49:31 UTC