Re: SUO: Re: Proposed SUO Content Outline
>¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>
>John Sowa wrote:
> >
> > I agree with Jon's point:
> >
> > > The problem is not writing the axioms --
> > > the problem is drawing the consequences.
> >
> > But I would add the more difficult problem of trying to decide
> > which axioms have consequences that can peacefully coexist with
> > the consequences of all the other axioms in the very big SUO pot.
>
>Exactly. This is what makes ontology-building an iterative process,
>at any rate, once it gets going at all. You deduce the consequences
>of your initial trial axiom set, at which point you will typically
>find that your "system of belief" (SOB, yes, in the sobering sense)
>crashes in either one of two ways:
>
>0. Into the Ground -- which means that you never quite get around
> to being able to derive any theorems that were not already as
> evident and as obvious as the axioms themselves, or as little.
>
>1. Into the Sky -- which means that all statements are theorems now,
> that the axiom set hides a contradiction and is thus inconsistent.
> It is the possibility of this higher way of crashing, and the fact
> that it is in practice the most prevalent way to go, that renders
> most of what you hear about "non-monotonic reasoning" utter jive.
> What all of this rap really means is that people typically respond
> to the threat of inconsistency, in the way that most varieties of
> religion have always done, by weakening their inference rules to
> the point where almost no contradiction can actually be derived.
No, Jon, you are too pessimistic. This isn't in fact where most
ontology efforts crash, or most AI Krep efforts either. In fact, a
LOT of axioms have been written which are neither trivial nor
inconsistent. God knows, I am not one who minimises the difficulties
of this enterprise, but I must defend an entire field from such a
trivial and wildly exaggerated accusation. And nonmonotonic reasoning
is not"utter jive", but a well-researched area with its own quite
powerful notions of inconsistency. You could take a look at
http://www.dfki.uni-kl.de/ruleml/ for a summary of recent work.
>And here, at the outset of this prospectively recurring cycle,
>is where we discover that we are not likely to get very far
>without the utility of some very powerful theorem provers.
Such things are indeed very useful. However, the vast majority of all
the axioms ever written can be phrased in languages which have quite
efficient theorem-proving algorithms, such as description logics in
the CLASSIC mold: see
http://www.cs.utexas.edu/users/mfkb/related.html for an overview of
current projects and applications.
Pat Hayes
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes