Re: SUO: Re: Industry takeover
Andrei,
I believe that we have removed the inconsistencies you're referring
to. I'd suggest trying the latest version. I think the version you worked
on was from last summer, before we had a chance to check SUMO with theorem
provers such as yours. I think it's great that you're working with SUMO.
Adam
At 08:19 PM 4/30/2003 +0100, Andrei Voronkov wrote:
>Hi everyone,
>
>I am new to this mailing list and cannot follow all aspects of the
>discussion easily, but I can add some remarks to John's recent letter.
>
> > 3. Is there a proof of the consistency of the ontology
> > as a whole (i.e. by a theorem prover that would
> > have been able to detect an inconsistency, but
> > terminated in a finite time without detecting any)?
>
>There can be no proof of this kind for two reasons.
>
>1. All versions of SUMO we played with are highly inconsistent. We ran
>our prover Vampire in quite a simple mode and have been able to detect
>many inconsistencies in it. I mean MANY. Dozens. We are working on a
>special mode for long inconsistency-detecting runs. [Note: we worked on
>a first-order version of SUMO specially made for Vampire by
>Teknowledge].
>
>2. Even if you remove all inconsistencies detectable by the existing
>theorem provers running for months there is a little chance to ensure
>the inconsistency of the whole SUMO: it uses quite complex statements
>(some with equality) which are outside of all standard decidable classes
>of first-order formulas; and it is very large.
>
> > There are other claims that I also find incredulous,
> > such as the notion that a monolithic ontology is
> > desirable. Cyc gave up that idea a dozen years ago,
> > but it has still been claimed as a desirable goal for SUMO.
>
>I agree with this. More structure is required, not only for the sake of
>consistency, but for tractable (in a practical sense) reasoning.
>
>As for IFF, I do not know the project well enough to make any
>judgement. However, as a specialist in automated reasoning, I do not
>know any REASONING related project based on category theory. What I mean
>by this is that I don't know any attempt of formalizing math or other
>applications in category theory so that one can use theorem provers for
>reasoning. However I would like to emphasise that I am not an expert in
>this: maybe IFF is not about reasoning at all?
>
>By the way, SUMO now contains several features making it unfriendly to
>reasoning as well (most notably row variables and the lack of
>structure).
>
>AV