Re: SUO: Re: Industry takeover
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