Re: SUO: Re: CG: Re: Common Logic Standard
Bill Andersen a écrit :
>
> On 4/6/02 18:21, "John F. Sowa" <sowa@bestweb.net> wrote:
>
> >
> > Jon,
> >
> > There is much more to knowledge representation than just FOL.
> > FOL is a prerequisite to any and every full-bodied knowledge
> > representation. It is necessary, but not sufficient.
> > But nonetheless, it is necessary.
> >
> > Bottom line: If we don't provide FOL plus contexts plus metalevels
> > (as the CL standard is designed to do), we are going to be stuck
> > with kludges built on top of RDF and XML for another 50 years.
>
> John has made my points much more effectively than my lame attempts to do
> so. Point 1 was that FOL *must* be one tool in your toolbox - there will
> undoubtedly be others. Point 2 was that FOL has enough expressive power to
> do the vast majority of what we need. Neither of which is to be read as an
> endorsement of KIF or any other concrete syntax.
Sorry, I don't agree with point 2.
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
it's *proving* capabilities, in spite of being truly *awkward*, are indisputable.
Here I mean that once you proved something with the HOP TP, the residual
doubt about the veracity of the proven statement which stems from the
possibility of bugs, clerical errors etc... is *extremely* low.
SECOND, I will say that the childish attempts to expel troublesome
consequences of "high order" constraints while still retaining their
usefull expressive power are doomed to fail, such as you pointed out
yourself in: http://suo.ieee.org/email/msg08207.html
> But they (the philosophical assumptions) have real impact. Necessarily
> existing properties? No problem: OIL (or any DL) has 'em! No theory of
> identity? No problem: different name -> different object! Relational
> properties (e.g. "Italian")? No problem: they don't exist because they
> cause computational problems.
As Russell (not always so bad...) said once:
"One might as well, in talking to a man with a long nose, say:
'When I speak of noses, I except such as are inordinately long',
which would not be a very successful effort to avoid a painful topic."
(In "Mathematical Logic as based on the Theory of Types", 1908)
Because, no matter how you disguise the underlying *high order*
constraint it is still here and still *high order*!
Why not dealing with the fact up-front?
The RDF people are struggling with "reification" because they do not
want to recognise that, in many cases, it amounts to high order statements.
Trying to hide that results in incredibly contrived definitions which
make it *even more* difficult to find one's way toward some solution.
---
A likely way to eat our cake while still keeping it could be a change
in some of our underlying (yet unheeded) assumptions.
A) Who said that *anything* coming from some external source should be
taken at face value, even if we summaryly check it for plausibility?
B) Who said that to check for consistency of a bunch of statements you
throw them altogether in the same bucket and then try to derive a
contradiction, or even worse a consistency proof which might well be
just semi-decidable (on the *wrong* side of the "semi" of course!) ?
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*".
An exception could be made for "analytical" (a.k.a. formal) knowledge.
If someone sent you a new mathematical theory and you checked it's
soundness with respect to a set of axioms you agree with, it is just
as good for *you* as your own homebrewed knowledge.
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.
Thus, only when trying to merge knowledge from different sources, one
would have to care for the "difficulty" of proof searching.
More on this point further below.
Which leaves us with the "difficulty" of the proof for the knowledge
authors themselves, there is way out of that too.
The name of the game is "definitional extension".
In definitional extension you have to prove all the steps that lead
to a new statement you propose, a (preferably large) part of it has
to be automated of course, but this need not be a *blind* search for
the theorem proving component of your ontology building software.
Whenever you are elaborating a new piece of knowledge, you know what
you are talking about (spozedly...) and you can *drive* the theorem
proving component with *hints* about how to come up with the intermediate
deductive steps between statements you want to prove true.
In HOL these are called "tactics" and are (unfortunately, bad design...)
heavily dependent on the implementation language ML, but this is another debate.
Yet, this policy is of no help for factual data:
"I just saw an Unicorn."
But in this case we rely on point 'A'. This is some kind of an axiom
on *your behalf* with wich others may agree or not or even ponderate
with trust coefficients that they can compute and manipulate in any
way they see fit for *their* purposes.
A small digression. I am strongly against any kind of "fuzzy" logic
or bayesian or otherwise statistical coefficients to be part of the
definition of ontology interoperability. This is, and should only be,
anyone's private concern.
Also, please notice that, if you start making more statements about
your "Unicorn", you *have to* provide for the internal consistency
of these statements, make the relevant proofs and have them available
along the Unicorn story.
(A pre-emptive strike against nit-pickers: In creating these proofs
the author has only to care about *his* logic theory which he will
have to provide to third parties along with the Unicorn stuff.
They have to make sense of the stuff as a *whole*, both the Unicorn
story and the logic upon which it is built.)
---
Now, about "merging" knowledge from different sources while preserving
consistency.
First note, that, trying to achieve this, implies that for some reason
the receiving party has the intent of "approving" the knowledge it
received, whether because it is a *formal* knowledge or because for
"authoritative" reasons it *has* to approve this knowledge.
Otherwise, there is not much reason for trying to ensure consistency
between two different "realms" of knowledge, they can very well live
within the same ontology without conflict provided that it is known
that they came from different sources and are kept separate.
This is the case for Cyc microtheories, but I am not sure my argument
is in support of them because Cyc microtheories are *not* guaranteed
not to be ultimately used together (uncaring of consistency checks).
Then, before dealing with the reconciliation of the meanings of any piece
of knowledge between two parties, there *must* be some common shared and
agreeded upon antecedent up the chain of "ontological" premisses from
both parties, otherwise NO communication would be possible.
(A quick note: ontological premisses are the "meta" statements,
i.e. what does the word "meaning" means...)
The possibility of *any* communication at a given time depends on how
well the current "topmost" (or latest, or deepest in chain, depends on
your view...) ontological premisses of each party can be first brought
into some "correspondance" or translation in the terms of the other.
The first step is to get both sets of ontological premisses from each
side somewhat "in synch" by mutual translation and consistency check.
So, the present argument applies recursively "up the chain" of ontological
premisses of each side until the common shared antecedent is reached.
The second step is to translate the new concepts embedded (possibly) in
the piece of knowledge you want to check with a process similar to
what I suggest in: http://suo.ieee.org/email/msg08132.html
The third step is to actually check the consistency of all assertions
coming from the new piece of knowledge, and YES this may be formally
indecidable or even even just intractable which is practically not
really better.
BUT! Remember? The consistency proofs of the new knowledge have been
given to us by the other side.
If we succesfully unwinded the recursion from the common shared ontological
premisses, we already have ALL steps translated into *our* formalism from
there up to the the new assertions we want to check.
There may still be some work left to do, I did not investigate that matter
further, but this is NOT THE SAME GAME LIKE STARTING FROM SCRATCH!
Gotcha?
If not, read it again from: Now, about "merging" knowledge...
> As for Jon Awbrey's accomplishments in theorem proving, I say great! But I
> think he and I are using the term "ontology" to describe very different
> things. All I want is for a computer system, for example, to be capable of
> detecting that a model that has a person being older than one of their
> ancestors is a bad thing, and to be able to communicate that information to
> other computer systems that claim to represent information about people,
> parents, ancestors and so on.
>
> I am NOT talking about the ability to prove novel theorems in mathematics.
Well, no, just about something that has *equivalent* power!
So, you better bite the bullet.
> As a builder of systems to represent information in such a way that sense
> can be made of it, that it can be kept consistent with the agreed upon
> meanings of terms in a community of use, and that it can be exchanged freely
> within such communities, I am interested first and foremost in doing the
> mundane things right. Once that is done, then maybe we can worry about
> doing novel things. But we don't even do the mundane things right at this
> point.
I am gratefull you acknowledge that, as opposed to some others (everyone
will recognise them..) who claim, if not present, imminent success.
But do *you* have any suggestion or even just a vague clue about
how to do the "mundane things" right, as of today?
> I challenge Jon (or anyone else) to give one example - just one - of some
> *practical* representation task, having a bearing on the ontology task as
> stated above, that cannot be done with FOL in whatever syntactic guise.
> Actually, I can think of one - defining a relation to be finite - which I
> understand is not expressible in FOL, and may be useful on a practical level
> (not sure of this) for communicating the meaning of a term to a peer with
> whom one (or some system) may want to communicate. So, I admit that there
> is room for more tools and principles.
>
> But, saying things like:
>
> > [JA] Logic today is in a horrible mess -- it is dissociated from all of
> > the real action in mathematics, programming, and science generally, and
> > it is not fair to blame Peirce for the state that has resulted.
>
> doesn't help. What is it exactly that Jon (or, not to pick on Jon, anyone
> else) wants to do that requires that this "mess" be supplanted by other
> principles. Why is it that we should be concerned with "the real action" in
> mathematics, for example, if we can't even at this point, as I've stated
> before, exchange my address book between a Palm Pilot and an email program
> without screwing it up? If someone could demonstrate that, rather than just
> talking in vague generalities, folks (including myself) may become more
> inclined to listen.
I did not check yet, but if it can be demonstrated that in order to
properly define the meaning preservation in the "address exchange"
process you need high order logic to describe *some* parts of it,
would that make you more affectionate for "real action in mathematics" ?
Best.
-- Jean-Luc Delatre
------------------------------------------------------------------------------
"Any resemblance between the above views and those of my employer,
my terminal, or the view out my window are purely coincidental.
Any resemblance between the above and my own views is non-deterministic.
The question of the existence of views in the absence of anyone to hold
them is left as an exercise for the reader.
The question of the existence of the reader is left as an exercise for
the second god coefficient. (A discussion of non-orthogonal,
non-integral polytheism is beyond the scope of this article.)"
-----------------------------------------------------------------------------
http://perso.club-internet.fr/jld/ -- GSM: +33 6 11 24 06 29