SUO: Re: Common Logic Standard
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.
> 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.
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.
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.
> 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.
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.
John Sowa