Re: Quoting and unquoting variables in KIF

sowa <>
Date: Tue, 13 Apr 93 01:56:03 EDT
From: sowa <>
Message-id: <>
Subject: Re:  Quoting and unquoting variables in KIF
Cc:, interlingua@ISI.EDU,

Yes, I'm not completely satisfied with those 4 or 5 conditions
that I stated in my last note.  But at least they are a step in
the right direction:  they don't cause all tautologies and
mathematical theorems to collapse into the constant T and
they restrict the proofs to logical transformations that do
not incorporate any background knowledge or definitions.

What they do is to provide a way of defining "proposition" in
terms of formal languages and grammars.  With different languages
and grammars, you would get different definitions of what it means
to be a "proposition".  But the range of variation would be within
relatively controlled limits:  at one extreme, you would have the
Lindenbaum algebras with very large equivalence classes (i.e. all
tautologies map to T); and at the other extreme, you would have
one formula per equivalence class (i.e. every formula expresses a
different proposition).

I would like to add another condition or two to my definition
that would tighten up the constraints and produce something
that corresponds fairly well to the intuitive notion of what
it means for two statements in two different languages to 
"say the same thing."

In the work on mapping conceptual graphs to and from KIF,
the mappings I've defined correspond quite well to what I
would like to call a "proposition".  But I'd like to generalize
those mappings to a set of guidelines or constraints that could
be used by people who would like to add other languages to the
same family.