**Mail folder:**Interlingua Mail**Next message:**FWLIV@delphi.com: "Re: attitudes to Krep"**Previous message:**olsen@cs.stanford.edu: "C++ KIF Parser"**Maybe in reply to:**Fritz Lehmann: "Higher-Order KIF and Conceptual Graphs"**Reply:**Tom Gruber: "what is the "all" in KIF's forall ?"

Date: Fri, 03 Dec 1993 10:02:16 -0400 (EDT) From: FWLIV@delphi.com Subject: Higher-order KIF and Conceptual Graphs To: interlingua@ISI.EDU, boley@dfki.uni-kl.de Message-id: <01H61EPH75PE92000I@delphi.com> X-Vms-To: INTERNET"interlingua@isi.edu,cg@cs.un mn.edu,boley@dfki.uni-kl.de" Mime-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-Transfer-Encoding: 7BIT

Dear Tom Gruber: Gruber@HPP.Stanford.edu No-one disputes that KIF has function and relation objects. The "logic order" issue is about the semantics of quantification over them --- whether it's based on "weakly" (actually First- Order) vs. "strongly" higher-order logic. The former allows quantification only over a specified set (based on a currently available vocabulary) of relation-symbols, whereas the latter can genuinely quantify over all relations irrespective of the particular currently available vocabulary. I listed all examples mentioned in this stream, expressly including some "weakly" (i.e. KIF if it's FO) definable, and some not. In your last message to these email lists you worked out the first page of my examples, but these were not the proved cases requiring strongly higher-order semantics, which were mostly on the last pages. Although you are at the core of the Knowledge Sharing Effort, and probably KIF's main user, you mention "KIF, which I am told is first order." The rest of us are in much the same position, having constructs like "(relation ?r) ... (forall ?r (r? x?))" which looks higher-order but which we are "told is first order". Your examples in KIF with "forall ?r"s and the implict foralls in KIF rules with "=> ?r ..." do nothing to address the issue of what relations these quantifications actually cover. I'll curtail my tenaciousness on this; Pat Hayes and others and I have covered the issue at length, an issue I doubt many on these email lists had known about before, and we cited references. There are certainly: A. higher-order concepts of practical importance for knowledge-bases and AI, and B. concepts which are only strongly-higher-order definable. Where A and B overlap, there is a problem for KIF. For Conceptual Graphs, John Sowa has already addressed the overlap a bit: he has now departed from FOL by (wisely, I think) including natural numbers as primitives along with a "cardinality" function from a set to a number. Using these he defined "connected" and "finite" (which are not First-Order-definable). A type lattice on differentia graphs with CG "actors" would require a further departure. I'm grateful to Sowa for recommending Gordon & Melham's "HOL" book, which as far as I can tell does things right. (It includes beta-reduction and if there's "First-Order- ism" hidden in there, I haven't found it yet.) One could do knowledge interchange using the implemented, fully formalized, typed, higher-order, ML-based "HOL" language itself. Still, Tom, your long message deserves response. Those who find this (foundational rather than notational) discussion pointless, stop reading now -- and use your kill file! >This work falls in the pragmatic side >of Pat Hayes' dichotomy: i.e., the purpose of the ontology is to >facilitate communication and not to prescribe the cognitive structures >of the agents. Yes. Pat's description of our big difference was correct (if applied to knowledge interchange rather than Krep in general), and I look to interchange-language semantics for unambiguous communication rather than for determining the whole of "meaning" for an agent. In most domains every description is only an approximation. There will indeed be predicates like Pat's "VERY- BIG" example. In practical knowledge interchange there will always be part of the language (in fact most) which gets its meaning from outside the formalism. This is far short of Pat's vision of "grounding" all meaning with a complete formal semantics. >The difference between KIF's higher-order relations and >a second order semantics, I gather, hinges on just what is being >quantified over when one says "for all relations...". Yes, assuming KIF's "higher-order" relations are actually First-Order. Not only "for all relations..." but also "there exists a relation..." is affected. >For pragmatic purposes such as those mentioned by Fritz Lehmann (e.g., >comparing databases), I have never seen an example where one actually >needs to quantify over all the theoretically possible relations. The >constraints of finite computation ensure that the set of relations of >interest will surely be describable in the finite vocabulary >(otherwise how could you even print out the answer?) and therefore >countable. Of course this is understating the case: the set of named >relations in any implemented database (or concepts in a terminological >subsumption lattice) will be quite small. There's more to Krep than comparing databases. In particular, very different ontologies need to be integrated; one may be a straightforward finite database and the other a highly abstract domain. A CAD database may need to exploit and interact with an abstract axiomatization of geometry and perhaps a graph-theory concept system. The latter have infinite "spaces" of predicates and relations, some of which are undefinable in First-Order (called "strongly higher-order" in my updated list of examples with references). An integrator will need to quantify over them all, to correctly define things like identity of triangle objects, etc. (see below). > ...the >semantic account for KIF (by which two moderately educated humans >might agree when A implies B)... When the relatively uneducated (the users) rely on the moderately educated (the AI people) to correctly implement concepts well understood only by the very highly educated (the relevant mathematicians), like higher-order model-theoretic semantics, caution is advisable. This applies especially in order to correctly "agree when A implies B". >But let's see the evidence: >>1. "Aristotle has all the virtues of a philosopher." >One man's virtue is another man's vice (type X). If this example is >meant to suggest that property inheritance requires higher order >logic, it doesn't. If (instance-of aristotle philosopher), then any >property P that is asserted of all philosophers applies to aristotle. >Taking classes to be unary relations, to assert a property of a class >is to write a rule of the form (=> (philosopher ?x) (p ?x)). From the >definition of instance-of, it follows that (philosopher aristotle). >(p aristotle) holds by universal instantiation. This is wrong because the sentence nowhere states that Aristotle is a philosopher (he may lack their vices), so inheritance is not involved. Your phrase "any property P" is higher-order and a "(forall ?p)" has to be added if your KIF implication "=>" is to apply to more than just the one predicate "p". My formalization was "AP( (Virtue(P) & Ax(Philosopher(x) -> P(x))) -> P(Aristotle) )". Granted, this is easily expressible in KIF with a "(forall ?p)" but the question of what predicates "forall ?p" actually covers remains unresolved. >>2. Patrick Winston's relation-between-relations semantic net >>link [between the "left-of" and "right-of" relational links]. >This depends what you want the relation-between-relations to mean. >Here's an example of a relation-between-relations that I assume can be >understood from its first-order definition: > (<=> (INVERSE ?r1 ?r2) > (and (binary-relation ?r1) > (binary-relation ?r2) > (<=> (holds ?r1 ?x ?y) > (holds ?r2 ?y ?x)))) >If you don't like HOLDS, you can do the same thing using sets of >tuples. Yes, this does it. Of course variables like ?r1 and ?r2 which appear in a KIF implication without a preceding quantifier are deemed to be universally quantified (page 22 of KIF 3.0 Manual), so there are implicit "forall"s and again the issue (of what is quantified over) is unresolved. >>3. The IS-A link in inheritance and subsumption hierarchies. >>[as a relation or link, not a set of FO axioms] >IS-A is instance-of as defined above. I use IS-A for AKO (subtype) as opposed to instance-of. Both are easily expressed in KIF, subject to my comments on examples 1 and 2. >>4. The relational IS-A/subsumption link in relational >>hierarchies. [some arguments may be permuted] >I don't undestand the "permuted" comment, but here is relational >subsumption: >(<=> (SUBRELATION-OF ?child-relation ?parent-relation) >. (and (instance-of ?child-relation relation) > (instance-of ?parent-relation relation) > (forall ?tuple > (=> (member ?tuple ?child-relation) > (member ?tuple ?parent-relation))))) Again, "?child-relation" and "?parent-relation" are implicitly quantified over, so the logic-order question remains. [The "permuted" deals with relational symmetries. Tuples are sequences in which every argument position is distinguishable, so an n-adic relation with some symmetries among its (indistinguishable) arguments will be repeated in the relation as multiple tuples with the positions of symmetric (but somehow distinguished or named) arguments permuted. Assuming this, your definition handles it.] >>5. The formal definition of individual identity or equality. >>[As in "x = y =def= Ax,y AP (P(x) iff P(y)).] >Equality is a primitive operator in KIF. This is Type X again. What >do you mean by "AP"? If one takes equality as primitive, then by >substitution all the (<=> (P ?x) (P ?y)) axioms will be true. What >else do you need in order to communicate the meaning of a knowledge >base full of P's and x's? Of course if equality is truly primitive it needn't be defined at all. But you mention "by substitution" (of "all" P's of course); the ability to substitute is exactly what this definition (Leibniz's) implies. "AP" means (forall ?p). You kindly didn't point out my egregious error of including the "Ax,y" (which effectively limits the universe to one kind of object!); it belongs to the left of the whole definition. I corrected this in the updated list of examples. This equality business is serious in Krep practice. It is by no means obvious when two objects in an ontology are "the same object". This often needs to be formalized. In purest unlabeled graph theory, for example, two graphs are the same if they're isomorphic; in fact TWO such graphs cannot be isomorphic -- they are the same graph. Some geometry systems identify congruent triangles (even if reflected), yet a CAD system has to distinguish them as separate objects. In manufacturing, "a part" may or may not be one physical object in the world; it may be only one object with respect to the device it's part of, but have many counterparts in identical devices (the ontology may well not have "available vocabulary" to distinguish it from these others, in a FO system). This issue is closely related to my examples 25 and 35. >>6. The assertion that, for a particular individual, all of a >>certain kind of functions on that individual take a certain >>kind of value. [including recursively defined functions] >Here is the case for a specific function on a particular individual: >(<=> (VALUE-TYPE ?instance ?binary-relation ?type) > (and (instance-of ?binary-relation binary-relation) > (instance-of ?type class) > (forall ?value > (=> (holds ?binary-relation ?instance ?value) > (instance-of ?value ?type))))) >Using that, we can generalize to "all of a certain kind of functions": >(=> (certain-kind-of-function ?f) > (value-type particular-individual ?f certain-kind-of-value)) Again, both ?binary-relation and ?f are implicitly universally quantified here. If KIF is only First-Order, then these fail to cover all of the desired functions (unless certain- kind-of-function happens to mean "first-order-definable-function" or a subset of that!). >>7. The ability to refer to and predicate the relations which >>exist between a given relation and its own arguments. For >>R(a,b), this yields R'(a,R); R''(b,R,R'); and infinitely more. >The following defines the function mapping a relation to the class of >all objects that are one of its arguments in one of its tuples. >(<=> (RELATION-UNIVERSE ?relation ?type-class) > (and (relation ?relation) > (class ?type-class) > (forall (?x) > (<=> (exists ?tuple > (and (member ?tuple ?relation) > (item ?x ?tuple))) > (instance-of ?x ?type-class))))) >With this vocabulary you can a define you favorite specialization of >"relations which exist between a given relation and its own >arguments". So, if I follow the notation above, R'(a,R) would be >(<=> (r-prime ?x ?r) > (instance-of ?x (relation-universe ?r))) >or perhaps order matters: >(<=> (r-prime ?x ?r) > (exists ?y (holds ?r ?x ?y))) >and that is a special case of the frame-ontology's EXACT-DOMAIN. The last definition seems to do it for a fixed-arity dyadic relation ?r. Perhaps you could handle poly-arity relations too. I mentioned this and several related cases in connection with C. S. Peirce's "hypostatic abstraction" of relations into individuals after Mike Genesereth had remarked that no such relation as r' exists. The connection of these examples to logic-order is a little different from the other examples. Having r-prime itself as a relation now recursively creates an infinite number of relations as soon as one ?r is asserted. Consider that (kappa (?z ?r) (r-prime ?z ?r)) applies to itself, etc. I suggested that the totality of such relations might be unreachable by First-Order quantification on relations; Chris Menzel replied that quantification with (First-Order) Henkin semantics would cover them. I'm not sure. I guess it could reach the members of any particular one, but I don't know that it can cover the recursive closure of all of them. Anyone have a good reference? >8. Semantic "case relation" taxonomy links. >Type X. If you can explain what this means using only email and no >references to literature I don't have time to read, I will write the >axioms in KIF. If you mean "referring to the nth argument of a >relation tuple", that is trivial (see NTH-DOMAIN). I won't go into deep-case theory, which involves the intension. It's not NTH-DOMAIN but rather the "type" of the role as opposed to the type of the participant. A particular set of r- prime relations (as above) shares with others certain features in common. This induces a relational hierarchy combining the methods of examples 4 and 7.. Thus a participant in a relation has a meaningful "role" in the relation, which role has qualities in common with similar roles in other distinct relations. By this you can generate AGENT, VICTIM, SPATIAL-PARTICIPANT and similar semantic "thematic" roles used in linguistics and semantic networks. KIF could do the extensional part of this using your methods in 4 and 7. >>10. The inclusion ordering in cylindric algebras. >In the engineering math ontologies, we've axiomatized textbook >abstract algebra using the same sorts of second-order notation >described above. Relations in KIF are based on sets. Cylindric Algebras in general (unlike some other abstract algebras) are not representable as systems of sets if they include triadic relations. (Only so- called Regular Locally Finite Cylindric Set Algebras are.) This was proved by the mathematician Lyndon and Henkin, Monk, Tarski and others for various classes of unrepresentable Cylindric Algebras. So I surmise that KIF would not be able to express them with correct semantics. (Brink & Schmidt's article in my "Semantic Networks" collection showed that KL-ONE-type systems are notational variations of well-known members of this general family of algebras.) > Say exactly what you mean, and I'll say it in KIF. >tom A generous offer. Things like "x is finite", "x is a natural number" "x is connected" and all the only-strongly- higher-order-definable things can be said in KIF, but I don't see how the formal semantics will be correct if KIF is First- Order. You can say it in KIF, but it won't be exactly what I mean. Fortunately I'm unwilling to say exactly what I mean, if it means I have to formalize in higher-order logic the 58 examples I listed. I think I've done enough on email to alert the KIF and CG communities to the logic-order issue. Yours truly, Fritz Lehmann fritz@rodin.wustl.edu 4282 Sandburg, Irvine, CA 92715 USA 714-733-0566 ==================================================== .