SUO: Re: OpenCyc Released
Comments below.
Jay
----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Jay Halcomb" <jhalcomb8@attbi.com>
Cc: "Standard-Upper-Ontology (E-mail)" <standard-upper-ontology@IEEE.org>;
<cg@cs.uah.edu>
Sent: Friday, April 05, 2002 11:15
Subject: Re: OpenCyc Released
> Jay,
>
> My concerns about OpenCyc are based on my concerns about Cyc,
> which are mostly based on what I've read and heard from many
> of the Cyc developers themselves and from other people who have
> used Cyc. As an example, I'm enclosing (at the end of this note)
> some comments about Cyc written for a workshop at IJCAI'2001.
>
> Jay Holcomb wrote:
>
> JH> What do you mean by 'consistent', John? Formally or informally
> > consistent, and with what further specification?
>
> By the usual definitions (either formal or informal), a set of
> propositions is consistent if and only if it is not possible to
> derive a contradiction (i.e., a statement of the form "p and ~p")
> from them. I would assume it is formally consistent if you use
> formal proof procedures and informally consistent if you use some
> informal methods. (But see the enclosed note for qualifications.)
>
> JH> How should it be determined if OpenCyc is consistent, either
> > self-consistent or with anything else?
>
> Can you derive a contradiction from either (a) the contents of
> OpenCyc by itself or (b) the conjunction of OpenCyc with the
> contents of some other system with which it is supposed to be
> interoperable?
>
> JH> What is OpenCyc's proof theory, e.g.? Until that is known, the
> > question of self-consistency in that formal proof-theoretic sense
> > can't be answered.
>
> Cyc has many different proof techniques, which can be invoked
> at various times under various conditions that are not clearly
> specified in the Cyc documentation. (See the enclosed note.)
What is needed, then, to assess the consistency of OpenCyc, or any other
ontology/inference engine, is a detailed specification of the various proof
procedures. How much effort is involved in this, with 'Open'Cyc? Is it
possible to get such a specification?
>
> For that reason, some people, such as Bill Andersen, have found it
> convenient to use Cyc to build a knowledge base, and then take the
> axioms out of Cyc and run them on a simpler, more clearly defined
> system that does have a well-defined proof procedure.
>
> So I would consider the consistency of OpenCyc under the assumption
> of a classical first-order theorem prover to be the best approach.
> However, I would like to quote the conclusion from the note below:
>
> When asked, contacts agreed that, in spite of a cursory check,
> it was possible that unknown contradictions might exist that had
> not, yet, been derived. In this sense, Cyc can only guarantee
> that its microtheories are not known to be inconsistent (or
> KS-consistent). Ideal terminology, such as consistent and
> derivable, is often not appropriate for use with a large or
> complex implemented system.
>
> This is one of the main reasons why I believe that any large
> ontology, such as Cyc or SUMO, should be presented as a collection
> of modules, each of which can be tested separately for consistency
> by running a classical FOL theorem prover.
I wholeheartedly agree. Until this is done, whatever else of (somewhat
dubious, so far) interest might be accomplished, SUO is largely spinning its
wheels.
>
> If there are any modules for which consistency cannot be proved
> by that method, then I would like to see a clear statement (i.e.,
> a warning label) attached to that module. There may be valid
> reasons for using such a module for some purpose, but the user
> should know precisely when and why a consistency check has not
> been done.
>
> John Sowa
>
> ______________________________________________________________________
>
> Some Observations about Cyc
>
> [The following comments on Cyc have been extracted from a paper that
> was presented by Stuart Shapiro at an IJCAI Workshop (citation below).
> The evaluation of Cyc is based on Cycorp documentation and on experience
> by the first author (Frances Johnson) during a Cyc training course.]
>
> Doug Lenat and Cycorp have developed Cyc [Cycorp, 200la] -- a large
> knowledge base and inferencing system that is built upon a core of over
> a million hand-entered assertions or rules about the world and how it
> works. This system attempts to perform commonsense reasoning with the
> help of this large corpus of beliefs (mostly default with some that are
> monotonic). It divides its knowledge base into smaller contexts called
> microtheories which contain specialized information regarding specific
> areas (such as troop movement, physics, movies, etc.). Belief
> revision is performed within microtheories or within a small group
> of microtheories that are working together, and the system is only
> concerned with maintaining consistency within that small group (as
> opposed to across the entire belief space). For example: in an
> everyday context, a table is solid, but within a physics context,
> it is mostly space (between atoms).
>
> A belief can have only one truth value, so no microtheory can contain
> both p and ~p. For example, ~p could be expressed as the proposition p
> with a truth value of false. The technique for maintaining consistency
> is to check for contradictory arguments whenever a proposition is
> derived or asserted into a microtheory. When contradictions are found,
> their arguments are analyzed, and a decision is made regarding the truth
> value of the propositions involved. Rankings of beliefs, however, is
> not a part of the system -- it uses specificity to determine the truth
> value of a default belief. For example: Opus the penguin does not fly,
> even though he is a bird, because penguins don't fly. If there can be
> no decision based on specificity, the truth value of the default belief
> is unknown. A default belief loses out to a monotonic one. And,
> lastly, according to Cyc trainers and other contacts, contradictions
> that are purely monotonic bring the system to a halt until they are
> fixed. During Cyc training, Johnson attempted to prove this last
> statement and failed -- revision was performed. The instructors were
> surprised, but thought the training interface might be the cause. We
> plan to explore this further, but it is an example of a system behaving
> differently than it is described.
>
> As mentioned [above], Cyc did not perform as described, and there must
> be some question as to other possible differences from design theory.
> Most specifically, Cyc literature [Cycorp, 2001b] claims to keep the
> microtheories consistent, for lack of a better word. When asked,
> contacts agreed that, in spite of a cursory check, it was possible that
> unknown contradictions might exist that had not, yet, been derived. In
> this sense, Cyc can only guarantee that its microtheories are not known
> to be inconsistent (or KS-consistent). Ideal terminology, such as
> consistent and derivable, is often not appropriate for use with a large
> or complex implemented system.
>
> References
>
> Cycorp [2001a] _Cycorp, Creators of the Cyc Knowledge Base_,
> http://cyc.com
>
> Cycorp [2001b] _Features of CycL_, http://cyc.com/cycl.html
>
> The original article from which these paragraphs were extracted:
>
> Frances L. Johnson and Stuart C. Shapiro, "Redefining belief change
> terminology for implemented systems," _Inconsistency in Data and
> Knowledge_, Working Notes from IJCAI'01, Seattle, Washington,
> 6 August 2001, pp. 11-21
>
>