**Mail folder:**Interlingua Mail**Next message:**sowa: "Higher-Order Logic"**Previous message:**Tomas Uribe: "Re: Higher-order KIF & Conceptual Graphs"**Maybe in reply to:**Tomas Uribe: "Re: Higher-order KIF & Conceptual Graphs"**Reply:**Fritz Lehmann: "Higher-Order KIF & Conceptual Graphs"**Reply:**FWLIV@delphi.com: "Higher-Order KIF & Conceptual Graphs"

Reply-To: cg@cs.umn.edu Date: Tue, 9 Nov 93 17:34:14 CST From: fritz@rodin.wustl.edu (Fritz Lehmann) Message-id: <9311092334.AA02203@rodin.wustl.edu> To: mrg@cs.stanford.edu Subject: Higher-order KIF & Conceptual Graphs Cc: boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@isi.edu

Dear Mike Genesereth, mrg@cs.stanford.edu I have gone back to "read the manual" as you suggested, though not all of it this time. I noticed a mistake of mine (back in September in my first email inquiry on this matter) when I made a reference to 'uninterpreted "holds"'. I had searched through the KIF 3.0 manual for "holds" but had failed to spot its definition (in section 8.3, Concretion). Yes, one can _refer_ in KIF to countable sets, and sets of these sets, as reified objects. (This includes relations if interpreted as sets of finite, "ordered" sequences of objects.) It isn't clear to me how actual quantification on (the recursive closure of) these objects has adequately expressive semantics, though, if the interpretation is only First-Order. As I said to Pat Hayes, it may just be that your method does preserve those concepts and equivalences which will occur in real applications, in which case I'm not critcizing. Let us know. You told me to be more explicit, so here goes. I don't understand how, after first defining a relation with kappa-abstraction, one can then predicate the "mixed-order" relations between it and its own arguments (though it may be possible). If this should be obvious from reading the manual, I missed it. I described the practical value of this in previous messages to the interlingua and Conceptual Graphs lists. Also, let's look an earlier example, Charles Peirce's (or Leibniz's) sentence: "Given any two things, there is some character which one posseses and the other does not." He was unable to represent this in his Beta (First-Order) Existential Graphs, on which Sowa's Conceptual Graphs are based. "Character" is an old word for predicate. (Modernly, it need not be monadic.) The point of this statement, which is a theorem in some concept-systems, a possible axiom in others, and false in still others, is to give a criterion for the distinctness of two individuals. Some database theories assume it and some don't. John Sowa requested that I formalize that sentence. In true second-order logic I'd say: "Ax,y (~(x = y) -> EP ((P(x) & ~P(y)) v (P(y) & ~P(x))))". The "Exists P" makes it second-order; the disjunction may be droppable. It is not obvious to me how to convert this correctly to First- Order KIF or Conceptual Graphs. Perhaps you will do it very simply. Apparently one cannot in the definition assume that distinctness of individuals is already defined. My motivation for this is that I am exploring automated knowledge base integration, which has practical commercial value. This means starting with two knowledge bases with very different concept-systems and taxonomies ("ontologies") and discovering automatically the correspondences (identities, inclusions and overlaps) between concepts (and relations) in one and those in the other, and then using these correspondences for combining the two into an integrated knowledge base. Another use of the correspondences is automatic translation from one knowledge system to the other. When the two systems "first meet," they mutually explore the highest, genuinely ontological, levels of their concept-systems in order to find some common ground for communication. I think of this as "ant feelers" when strange ants meet on a path. I'm hoping that KIF and CGs will be suitable knowledge languages for this. Finding out the criterion for distinctness is an early priority, so the truth of Peirce's sentence in an ontology comes up soon. In KIF all predicable objects are subdivided into the two disjoint classes of sets and individuals. (7.1). The problem here is to determine, for a particular ontology, when a pair of differently described objects refers to a set-object (of two individuals) or to one individual object (or singleton), and conversely, when a single description must denote just one individual or may denote multiple individuals. Speaking slightly imprecisely for brevity: in all systems I've seen, the more some individuals number, the fewer the predicates (descriptions or containing sets) they share in common; dually, the more the predicates (or containing sets), the fewer the individuals which they all apply to or contain. This forms an "adjointness" between individuals/tuples and predicates, in some cases a so- called "Galois connection". In pure First-Order systems based on finite sets, the Galois connection between the powerset of monadic predicates and the powerset of individuals is a dual isomorphism (of Boolean lattices). So, for the finite case at least, Peirce's sentence seems to be a logically-true theorem. I would guess (by Stone's Theorem?) that it's a theorem for the countable case. (I'm researching the n-adic case with identiity.). In higher-order, approximative and intensional systems, there is still a Galois connection, but it is no longer a dual isomorphism. Then Peirce's sentence may or may not be an axiom (as far as I can tell). In inchoative systems (in the sense of Parker-Rhodes' "Theory of Indistinguishables") there is a kind of adjointness but it does not look like a true Galois connection. Then Peirce's sentence is false. If any of this is wrong, someone please correct me. I've come across about 117 existing concept-systems and I'm still seeking and finding new ones. (The hope is to exploit some of the person-centuries of thought and work that have gone into existing concept-taxonomies and specialized thesauri.) All three types described above occur, and they potentially need to be able to communicate. Even if Peirce's sentence is somehow obliquely suggestible in KIF or CGs by an analogous logically-true First-Order theorem on sets, this seems to make it impossible to define concepts in systems in which it is inherently contingent or false. In higher-order logic there is no problem since the Peirce sentence is easily expressed. Maybe you can straighten me out on this point. Another important issue for me is the higher-order, large-scale structure of concept hierarchy, in particular the ability to factor it into separate, structured "aspects" (a.k.a. dimensions, facets, determinables, attributes, poset-factors, or Aristotelian categories). My KIF 3.0 manual (June, 1992) omits the axiomatization of numbers. At the end of October I asked: "'All monotonic functions of 42 have positive values.' Not very exotic, but can anyone express it correctly in KIF?" I would still like to see your answer, which might be trivially easy. The question is, does it really quantify over ALL monotonic functions? No matter how weird or recursive they are, they still have positive values for 42. (Incidentally, KIF's requirement that all systems support its complicated number scheme seems a bit burdensome for implementers. I wonder how many ontologies will actually need to use "cis (x)" --- the complex number "(cosin(x radians)+ isin(x radians)". Hey, if we all need to support complex numbers, why not quaternions? Cayley numbers too. And Sylvester numbers! What's the principle for the cut-off?) The concept "infinite" occurs in some form in many ontologies. If there is a First-Order KIF definition, what is it? (If the answer is "read the manual" please give page numbers since there's no index in my copy.) I believe that the usual version of "infinite" is only higher-order definable. Barwise & Feferman's model theory collection mentions numerous other notions definable in higher-order but not in First-Order, like countable, well- ordering, natural numbers, real numbers, etc., and the key properties of theories of things like ordered Abelian Groups, various kinds of automata, trees; topolological, compact & Hausdorff spaces; complete partial & linear orders, lattices, and Boolean algebras; Scott-type domains, probabilistic systems, etc. At least some of these have practical applications. It seems a shame to disqualify them all from representation in a "universal" knowledge representation language. You asked what I recommend. As my earlier messages have said, I tentatively favor true classical n-order, (poly)n-adic logic semantics, or at least something which will accomplish the same things in all practical applications. I'm not yet persuaded that incompleteness or uncompactness are important practical considerations for knowledge interchange. Yours truly, Fritz Lehmann PS. My very parenthetical comment to Pat Hayes about Cantor's Theorem isn't relevant to knowledege interchange, since very few people share my skepticism. fritz@rodin.wustl.edu 4282 Sandburg, Irvine, CA 92715 USA 714-733-0566