Re: SUO: Re: Industry takeover
Andrei Voronkov a écrit :
> 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.
AT LAST, someone involved hands-on in an effective (if still academic
and "bleeding edge") application of logic, you are heartily welcome.
(pardon me John, but Andrei is not in the same playing ground than CGers)
> 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.
This need more emphasis:
IT IS PREPOSTEROUS TO START WITH A "SEMANTIC MESS" AND HOPE TO CLEAN IT AFTERWARD.
Even if this is the "natural" trend to try to stick to "human oriented"
concepts to favor understanding by the non-cognoscenti, it is a dead end.
Consistency can only be achieved by the opposite route, taking some pain to
define "usefull" everyday concepts from sound primitives, building this
bottom-up and not top-down.
Even if it should not be forgotten that the resulting sound concepts will
only approximate the "intuitive" concepts, at least they will still be
sound and USABLE in automated inferences.
> By the way, SUMO now contains several features making it unfriendly to
> reasoning as well (most notably row variables and the lack of
> structure).
Yes, just more support for the above.
Cheers.
-- Jean-Luc Delatre
-----------------------------------------------------------------------
"The only justification for our concepts and systems of concepts is
that they serve to represent the complex of our experiences;
beyond this they have no legitimacy." -- Albert Einstein
-----------------------------------------------------------------------
http://perso.club-internet.fr/jld/ -- GSM: +33 6 11 24 06 29