I want to respond to some of the minor technical issues raised by Pat, but as
these aren't very important I will come back to them later. The crucial point
is the one about decidability and complexity, as this is where there always
seems to be some mis-communication about the goals of and claims for OWL. I
completely agree that being decidable is no guarantee that reasoning tools will
always work well in practice. We can imagine a graph with complexity classes on
the x-axis and robustness on the y-axis. Increasing complexity inevitably means
decreasing robustness. Robustness is a very important quality of reasoners from
a user POV -- what it means is that small changes in the input (e.g., the
ontology) produce only small changes in the performance of the reasoner. We can
think of undecidability as simply being a very high complexity class, i.e., one
where we can expect relatively poor robustness. (01)
OWL also has very high complexity, although not as high as "undecidable". In
spite of this it has proven possible to develop OWL tools that work well in
typical cases -- this wasn't an accident, it was a design goal for the
language. This has been crucial to the adoption of such tools in practice --
most users expect/require the reasoner to be both fast and reliable (always
give an answer, and always give the right answer), and they are surprised, not
to mention indignant, if this is not the case. The high complexity inevitably
means, however, that this good behaviour is not always robust -- small changes
to an ontology can result in large changes in performance, and some ontologies
are still difficult or impossible to deal with. Developing new optimisations to
improve performance on such (classes of) ontologies is an ongoing (and
inevitably never-ending) battle. (02)
For some users, this lack of robustness is not acceptable, and this is why OWL
2 includes several profiles -- language subsets where reasoning has a lower
worst-case complexity. This is not just of theoretical interest -- the lower
complexity means that we can develop reasoners whose performance is much more
robust. (03)
There are other user who have the opposite problem -- they want/need a more
expressive ontology language. Of course they could move out of the FOL subset
that is OWL. The result will inevitably be that reasoner performance is even
less robust. Given the existing SOTA for FOL reasoning tools the loss of
robustness w.r.t. typical OWL tools would be dramatic -- e.g., instead of the
reasoner occasionally failing to compute the answers to all subsumption
questions, it would invariably fail to do so. This may change with time, but it
is where we are now. Whether or not this is acceptable is a decision that only
users can make -- you pays your money and takes your choice. (04)
Bottom line: there is no "right choice" of ontology language. OWL is intended
to be good compromise between expressive power and robust tool performance.
Perhaps more important than the choice itself was making *some* choice.
Standardisation has allowed for the development of a range of tools,
infrastructure and applications that could previously only have been dreamt of.
Hopefully all members of the ontology community can see this as a positive
development. (05)
Regards,
Ian (06)
Response to some minor technical issues raised by Pat: (07)
When I said complete I really meant complete and terminating -- I was being
ruthlessly pragmatic and ignoring the fact that "false" answers could always be
returned if infinite resources were available. In fact most SOTA FO theorem
provers aren't even complete in this theoretical sense, because for efficiency
reasons they start discarding clauses when the clause set becomes
inconveniently large. In practice, this means that such reasoners are rarely
able to prove satisfiability (non-theorems) -- see, e.g., the experiments we
performed using Vampire (consistently the best performing FO theorem prover)
for OWL reasoning [1]. (08)
As for correctness, it simply isn't true that this is easy to prove. For
theoretical algorithms, soundness *is* typically easy to prove, where I use
soundness in the sense of returning only correct "true" answers to the problem
that the algorithm is "naturally" solving -- which is satisfiability in the
case of model construction provers, and unsatisfiability (theorems) in the case
of deductive provers. It is much more difficult to prove that the reasoner is
correct if it says "false". In the case of model construction, for example,
this means proving that if there exists a model, then the algorithm will always
succeed in finding one. Proving termination, which I take to be essential for
correctness in case the logic is decidable, is even more difficult. Finally,
the algorithms used in practice are *much* more complex and include a wide
range of sophisticated optimisations; this makes it *much* more difficult to
prove that they are correct (or even sound). (09)
Regarding my claim that reasoners are typically used in a way that is actually
incorrect, to the best of my knowledge none of the incomplete reasoners in
widespread use in the ontology world even distinguish "false" from "don't know"
-- whatever question you ask, they will return an answer. Thus, in order to be
correct, applications would have to treat *every* "false" answer as "don't
know". I don't know of any application that does that. (010)
[1]
http://www.comlab.ox.ac.uk/people/ian.horrocks/Publications/download/2004/TRBH04a.pdf (011)
On 1 Aug 2010, at 18:54, Pat Hayes wrote: (012)
> Just to correct a point of terminology:
>
> On Jul 29, 2010, at 4:48 PM, Ian Horrocks wrote:
>
>> OWL and CycL are not really comparable, because OWL is based on a fragment
>of First Order Logic that is known to be decidable, for which provably correct
>reasoning algorithms are known and for which effective implementations based
>on said algorithms are available.
>
> True, though the CycL reasoning engine also takes advantage of many of these
>decideable cases. (The real difference here is one of academic style: the CycL
>developers are ruthlessly pragmatic and do not care a whit for theoretical
>analyses of completeness or for proving correctness.) It should be stated also
>that proving *correctness* of a reasoner is usually fairly easy.
>
>> OWL's expressive power could, of course, be easily (indeed arbitrarily)
>extended if one were prepared to compromise on some or all of these design
>constraints. For example, SWRL extends OWL with Horn clauses (AKA rules), but
>the resulting language is undecidable,
>
> True. Strictly, it is semi-decideable.
>
>> and so only incomplete reasoners are available.
>
> False. "Complete" means that if a sentence is a theorem, then the prover will
>(eventually) tell you that it is. Complete reasoners (in this, textbook,
>sense) are available for FOL and indeed have been for decades.
>
> Ian is using "complete" here to mean "complete and decideable", which can be
>characterized as: if a sentence is a theorem, then the prover will tell you
>that - completeness - AND if it isn't a theorem, the prover will also tell you
>that it is not. Full FOL is not decideable in this sense. But even when the
>logic is decideable it can still be the case that the complexity of the
>decision process is arbitrarily high, and if you have to terminate it early,
>you are left in a don't-know situation, whether the logic is decideable or not.
>
>> In fact such reasoners are typically used in a way that is actually
>incorrect, in that failure to find an entailment is treated as a
>non-entailment, whereas it should be treated as "don't know".
>
> I dont think it is fair to say that they are *typically* used in this
>incorrect way. (?)
>
> Pat Hayes
>
>>
>> Regards,
>> Ian
>>
>>
>> On 29 Jul 2010, at 20:15, Zhuk, Yefim wrote:
>>
>>> Ian,
>>>
>>> Thanks for another great event related to OWL2.
>>>
>>> What is your opinion on CycL and CycML (see http://cyc.com)?
>>>
>>> From my point of view, this language is more expressive than OWL and has
>naturally embedded rules features.
>>> I used this language to describe complex objects and rule-based business
>scenarios.
>>> I think, this comes much closer to mimicking real world than OWL can
>provide today.
>>>
>>> Do you see this one as gaining bigger acceptance and getting to the level
>of a standard?
>>>
>>> Or maybe there are some limitations that I don’t see?
>>>
>>> Thank you,
>>>
>>> Jeff
>>>
>>
>>
>> _________________________________________________________________
>> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
>> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
>> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
>> Shared Files: http://ontolog.cim3.net/file/
>> Community Wiki: http://ontolog.cim3.net/wiki/
>> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
>> To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
>>
>>
>
> ------------------------------------------------------------
> IHMC (850)434 8903 or (650)494 3973
> 40 South Alcaniz St. (850)202 4416 office
> Pensacola (850)202 4440 fax
> FL 32502 (850)291 0667 mobile
> phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes
>
>
>
>
> (013)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (014)
|