Re: SUO: Re: Common Logic Standard
"John F. Sowa" a écrit :
>
> Jean-Luc,
>
> I agree with Chris Menzel about the need to distinguish true HOL
> from various methods for quantifying and reasoning about predicates,
> types, and propositions.
This distinction, based on *true* mathematical properties (I do agree)
of the underlying model is a BAD THING!
Let me explain.
Just as in your other reply to Bill: http://suo.ieee.org/email/msg08258.html
you put emphasis on the influence of external form onto seemingly
unrelated design decisions:
> Although I agree with Bill that after the external syntax has
> been parsed it can be mapped into any internal form that is
> suitable for the available algorithms, the differences in the
> external form have a strong influence on what internal forms
> the programmer chooses, and therefore, on the choice of algorithms.
I maintain that, if the "naive" approach to state a predicate, a function or
whatever, is such that *if* the underlying model were infinite the resulting
statement would be "high order" then, IT MUST STAY SO in it's structure.
Because this will lead to the best design decisions for implementation.
Just the same kind of argument like yours about graph syntax versus FOL.
If, just for the sake of boasting that you have *escaped* "high order"
you cram the statement into a first order or finitary model, you have
introduced *irrelevant* constraints that will creep into the design
and screw up the *good* structure.
Why not, then, define everything in terms of a good old Turing machine, Eh?
> > IMNSHO high order logic is needed, the only reason it has not been
> > seriously considered is that it is even more "embarassing" than FOL.
> > It "screws up" the theorem proving capabilities of any system in
> > which it is used even more than FOL, by blasting off the search space.
>
> > But that is *not* a good reason to reject it because there are some
> > ways around that problem that I will try to explain below.
>
> > FIRST, I must say that I am a big fan of the "HOL theorem prover":
>
> > http://lal.cs.byu.edu/lal/holdoc/Description/HOL-logic/HOL-logic.html
>
> First, I must also say that the HOL system, which I agree is a very
> interesting and very powerful reasoning system, does not really use
> higher-order logic. It actually uses a metalevel reasoning system,
> which can be expressed quite nicely with the contexts and metalevels
> provided by the proposed Common Logic Standard.
>
> Second, it is possible to use the sorts of a sorted first-order logic
> to represent whatever types, predicates, or relations one would like
> to reason about. Sorts are also being suppored by the CL standard.
HA, HA, (sorry...) I am gonna be a troublemaker again!
Something I already said on the list, but which really deserves REMINDING:
"I have been doing technology watch on AI/theorem proving/program
synthesis/knowledge representation for more than 20 years"
This is technology *watch*, just a *survey*, this means I don't go that
deep into the subject matters (yes CM ;->), just enough to figure out
what it's about, BUT, on the other hand I have seen *lots* and *lots*
of papers and I have a somewhat "global" or "statistical" perspective.
So, thanks to your announce: http://suo.ieee.org/email/msg08241.html
I read http://cl.tamu.edu/minutes/stanford-minutes.html
And apart from the usual scrambling around various boring
(yet needed, alas) syntactical issues I spotted *real trouble*!
"Sorted KIF"
I entirely agree that typing is needed to such a point that in some cases
you cannot ensure consistency if you do not have a typing mechanism.
But, from all I have seen on the subject I can tell you, typing is HELL!
You are going to be in DEEP SHIT for these reasons:
- There is *no* GOOD choice, only tradeoffs. This has to do with the
Godel stuff, no matter how *powerfull* the typing is there are always
things that are not expressible anymore once you choose a typing.
You can extend it but this is an endless process.
- Given the above, which kind of agreement do you expect to reach
thru committee debating?
- Adorning expressions with (necessary) typing restrictions give
rise to all sorts of nasty syntactical side-effects that will
complicate ever further the agreements on already painfull
syntactical issues.
Another place where some breakthrough would be welcome.
No idea what, but that certainly requires thinking "out of the box".
> Just a couple of brief comments on some of your other comments:
>
> > As for point 'A', I suggest that *all* knowledge incorporated in
> > an ontology and coming from *any* outer source should keep a qualifier
> > to that source: "such and such has been said by *those people*".
>
> I certainly agree. This is just one (of many) reasons why I believe
> that any and every ontology should be maintained as a partially ordered
> set of modules. Each module should have its own revision history with
> a certification by its developers, maintainers, and users.
I certainly would not trust *any* certification issued by human beings,
specially from working groups, charter organisations, experts etc...
There must be a clear separation between "analytical" certification
only about consistency, and for which mechanical proving is the *only*
reasonably reliable solution, and certification of factual data for
which just some kind of "reliability coefficient" of the provider
can be *estimated*.
> One reason for a partial ordering (one prerequisite for a lattice)
> is that it explicitly shows the dependencies of each module upon
> any others. No module can be more dependable or consistent than
> the conjunction of all the modules it depends on. The certification
> of any module can never be stronger than minimal certification of
> all its prerequisites.
>
> The other prerequisite for a lattice is the ability to combine the
> modules in any way that anyone might see fit. That includes the
> ability to find the minimal common prerequisites for both, and the
> maximal common implications of both -- which are also called the
> supremum and infimum of the two modules.
Right, right, but why bother to *describe* those things that should
just be the *results* of architectural design. I mean, the fact that
"The certification of any module can never be stronger than
minimal certification of all its prerequisites"
is just a *consequence* of a proper design of the closure of the
certification level thru modules.
> > As for point 'B', I suggest that consistency has to be proven by
> > the *authors* of a piece of knowledge and that the proof of
> > consistency is to be carried along with the knowledge itself.
>
> The proof of consistency is one important part of its certification.
> There may, however, be some modules for which consistency has not yet
> been proved. I would allow such modules to be registered, but with
> a warning label that stated that its consistency is unknown.
I would *not* really like to use anything which consistency is unknown!
> The requirement for certification, by the way, has not yet been
> addressed by either OpenCyc or SUMO. The only claim that the Cyc
> developers have made is that they beleive that they have corrected
> all the inconsistencies that they have found. That is similar
> to Microsoft's claim that they have resolved all reports of issues
> (i.e., bugs).
>
> I believe that the development of an appropriate certification
> method is essential before any kind of ontology might be considered
> suitable as an IEEE standard.
Be carefull about "appropriate certification methods", they may bite
back by denying you certification while approving ludicrous junk.
Cheers.
-- Jean-Luc Delatre
--------------------------------------------------------------
Don't mind criticism. If it is untrue, disregard it;
if unfair, keep from irritation; if it is ignorant, smile;
if it is justified it is not criticism, learn from it.
--------------------------------------------------------------
http://perso.club-internet.fr/jld/ -- GSM: +33 6 11 24 06 29