ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] owl2 and cycL/cycML

To: Pat Hayes <phayes@xxxxxxx>
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>, Bernardo Cuenca Grau <bcuencagrau@xxxxxxxxxxxxxx>
From: Ian Horrocks <ian.horrocks@xxxxxxxxxxxxxxx>
Date: Mon, 2 Aug 2010 13:15:33 +0100
Message-id: <CAFE7B03-3C68-401F-8C1A-C360C439AAF1@xxxxxxxxxxxxxxx>
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)

<Prev in Thread] Current Thread [Next in Thread>