Re: clarifying clarifying email@example.com (Pat Hayes)
Content-Type: text/plain; charset="us-ascii"
Date: Wed, 9 Aug 1995 01:18:02 -0500
To: firstname.lastname@example.org (John F. Sowa), email@example.com, firstname.lastname@example.org,
email@example.com, firstname.lastname@example.org, email@example.com
From: firstname.lastname@example.org (Pat Hayes)
Subject: Re: clarifying clarifying ontologies
At 9:23 PM 7/29/95 +0500, John F. Sowa wrote:
.... 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.
>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
Well, that would be nice.
Heres an old example from Russell. He was challenged to show that from 1=0
it followed that he was the Pope. He replied: if 0=1 then 1=2; the Pope and
I are two; therefore, the Pope and I are one. Its a joke but it illustrates
the point. Heres your knowledge base and you ask it whether John Sowa is
the same person and Pat Hayes,and it replies "yes". Maybe it uses three
assertions in its derivation each of which is perfectly consistent and any
two of which are, but which are together an inconsistent set. How are you
going to know?
The problem is how to allow 'lifting' from one context to antoher without
thereby allowing contradictions to be passed over. This can be done for
example by simply anot allowing any transfer from one context to antoher,
but then the context system is useless.
The technical problem is that a contradiction is a property of a set of
assertions. How can one build 'firewalls' which respond to a global
property of all the assertions that have been allowed to pass through 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.
Yes, that what I did for the time axioms also. (In fact, its a very good
exercise to try to build counterintuitive models.) However, this is exactly
what consistency proofs do: they build models (or, more precisely, give
algorithms for building models). The NP hard part is all in that "try to".
1916 Ivy Lane, Palo Alto, Ca. 94303 phone (415)855 9043