John, (01)
I agree with your points 1-5 below. However, I just want to point out that Ian
Horrocks has developed reasoners such as FaCT which count as application
programs. His group develops the HermiT and ELK reasoners which we use every
day in the development of the Gene Ontology (as well as numerous other
biological ontologies). I don't think it's accurate to characterize his work as
"ivory tower". (02)
On Nov 19, 2012, at 5:32 AM, John F Sowa wrote: (03)
> On 11/18/2012 7:06 PM, Pat Hayes wrote:
>> Ian's argument here is really an argument for *efficient*
>> decidability, and (to give him credit) this is exactly
>> what he is a world leader in providing.
>
> I agree.
>
> The only disagreement is over the issue of restricting the language
> to make it impossible to write undecidable statements.
>
> The solution they adopted in OWL DL is to force every model to be
> expressible as a tree, because their proof of decidability only
> works on tree structures.
>
> That means you say that a benzene molecule has 6 carbon atoms, but
> you can't say the atoms are connected in a ring -- because a ring
> is not a tree. It would get their theorem prover hung up in a loop.
>
> They buy their beds from Mr. Procrustes.
>
>> Ian's view is that logics that aren't decidable are simply faulty,
>> broken, inadequate, not of interest, etc.. Any "reasonable" logic
>> should be decidable.
>
> Ian is very intelligent, but he needs to leave his ivory tower
> and take a job where he writes application programs. There are
> many of ways of using logic, and theorem proving is *not* the
> most important:
>
> 1. Stating a query. An FOL query against a relational DB is
> not only decidable, it can be answered in polynomial time.
> If the fields are indexed, the most common queries can be
> answered in logarithmic time.
>
> 2. Stating a constraint. The issues about queries also apply
> to constraint checking.
>
> 3. Stating preconditions and postconditions for procedures.
> These are also reducible to constraints. For many applications,
> a good compiler can derive an efficient procedure from them.
>
> 4. Stating formal definitions for humans. This is a task that
> the Z notation people have been doing for years -- some of
> them on very large, mission-critical systems.
>
> 5. Knowledge representation. Systems like Cyc can use and reuse
> the same information in many different ways -- including all
> of above and more.
>
>> And as Ian had proposed the wording and I was objecting to it
>> on what most people thought were arcane technical/logical/academic
>> details, I lost the vote.
>
> This is why I believe that the six-month review process for an ISO
> standard is important.
>
> With the ISO procedure, Bob MacGregor, Doug Lenat, Roger Schank,
> and the entire world would have a chance to review the text
> and make their objections known.
>
> That would certainly have slowed down the process. But for
> something as important as a standard that is supposed to govern
> the entire web for years, you can't accept a decision based
> on the personal preferences of somebody who had never written
> an application program in his life.
>
>> I don't know what the complexity class of OWL Full is. Those who
>> care about such things are usually working on description logics
>> in any case.
>
> Those people have been publishing their ideas in obscure journals that
> nobody who has a day job ever reads. And that's where they belong.
>
> John
>
> _________________________________________________________________
> 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
> (04)
_________________________________________________________________
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 (05)
|