Re: clarifying clarifying ontologies

sowa@west.poly.edu (John F. Sowa)
Date: Sat, 29 Jul 1995 21:23:53 +0500
From: sowa@west.poly.edu (John F. Sowa)
Message-id: <9507300123.AA07511@west>
To: cg@cs.umn.edu, doug@csi.uottawa.ca, fritz@rodin.wustl.edu,
        phayes@cs.uiuc.edu, srkb@cs.umbc.edu
Subject: Re: clarifying clarifying ontologies
Content-Length: 2562
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk

I've been trying to avoid getting ensnared in these debates because
I'm desperately trying to finish my book by Aug. 1.  I told my publisher
that it is like Windows 95 -- it was supposed to be out last year, now
the complete thing will be out in August, but wait for the "tune up"
in November if you want something that works.  In any case, here are
a few comments:

>I agree that Joe shouldnt need to be bothered by issues like these. But he
>HAS to be, because if he is careless about them, he is going to get
>ensnared in inconsistency and (what seems like) paradox.

My analogy with Windows in my opening note could be applied here.
I recall Dijkstra's little gem of an operating system called "THE"
(see the May 1965 Communications of the ACM) in which he proudly
announced that it was proven to be bug-free in design and that only
one or two minor syntactic errors occurred during the development and
they were quickly caught.  I admire Dijkstra's attitude, and I share
his disgust at the sloppily designed systems and languages that have
been dumped on us -- and the ones we are forced to use today are
far more badly designed than anything available in 1965.

I believe that we can, like Dijkstra, design a context system
that is provably safe.  That means that the context system itself
will never run into an inconsistency or hang-up with a deadlock
or paradox.  But like Dijkstra's system, it would not guarantee
that every user context would be bug free.  It would simply
guarantee the security of the fire walls between contexts and it
would ensure that a context that blew up with an inconsistency
would not affect any context outside itself.

With a secure context system, people could use axioms that were not
yet proved consistent because they could isolate them from their
"mission-critical" stuff.  The context mechanism doesn't automatically
solve the problems, but it helps you to contain them.

Re consistency proofs:  Of course, they are NP complete.  That means
that you never attempt a direct proof.  Instead, you try to build a
model.  If you succeed, then your system is consistent.  If you
can't build a model, then you tinker with your axioms until you
have a set that allows you to build a model.  That's what Dijkstra
did for THE system:  he designed the axioms, showed that they had
a model, and then hand-coded the axioms into the programs.

Proving that a given set of axioms has a model is NP complete, 
but proving that a given model satisfies the axioms can be done very
efficiently -- in at most polynomial time.

John Sowa